1d474a2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'refs/remotes/upstream/master' into issue/2333

Conflicts: src/Idris/AbsSyntax.hs

commit1d474a2c28952999162ee7d4a130cc16771b8b0c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 3 Jun 2015, 18:45 (11 years ago) parent5542d1c 0bc0008

4 files changed+18−3

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3 src/Idris/Docs.hs+6−1 src/Idris/REPL.hs+3−1 src/Idris/REPLParser.hs+6−1

src/Idris/AbsSyntax.hs+3

@@ -641,6 +641,9 @@ setDepth :: Maybe Int -> Idris ()

641641setDepth d = do ist <- getIState

642642 put ist { idris_options = (idris_options ist) { opt_printdepth = d } }

643643

644+typeDescription :: String

645+typeDescription = "The type of types"

646+

644647

645648type1Doc :: Doc OutputAnnotation

646649type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "Type 1")

src/Idris/Docs.hs+6−1

@@ -1,6 +1,6 @@

11{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}

22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3−module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

3+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, pprintTypeDoc, FunDoc, FunDoc'(..), Docs, Docs'(..)) where

55import Idris.AbsSyntax

66import Idris.AbsSyntaxTree

@@ -317,3 +317,8 @@ pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "ty

317317 t (Str _) = PConstant NoFC StrType

318318 t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)

319319 t _ = PType NoFC

320+

321+

322+pprintTypeDoc :: IState -> Doc OutputAnnotation

323+pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>

324+ nest 4 (line <> text typeDescription)

src/Idris/REPL.hs+3−1

@@ -945,7 +945,9 @@ process fn (Core t)

945945 iPrintTermWithType (pprintTT [] tm) (pprintTT [] ty)

946946

947947process fn (DocStr (Left n) w)

948− = do ist <- getIState

948+ | UN ty <- n, ty == T.pack "Type" = getIState >>= iRenderResult . pprintTypeDoc

949+ | otherwise = do

950+ ist <- getIState

949951 let docs = lookupCtxtName n (idris_docstrings ist) ++

950952 map (\(n,d)-> (n, (d, [])))

951953 (lookupCtxtName (modDocN n) (idris_moduledocs ist))

src/Idris/REPLParser.hs+6−1

@@ -269,10 +269,15 @@ cmd_doc name = do

269269 c <- fmap fst P.constant

270270 eof

271271 return $ Right (DocStr (Right c) FullDocs)

272+

273+ let pType = do

274+ P.reserved "Type"

275+ eof

276+ return $ Right (DocStr (Left $ P.mkName ("Type", "")) FullDocs)

272277

273278 let fnName = fnNameArg (\n -> DocStr (Left n) FullDocs) name

274279

275− try constant <|> fnName

280+ try constant <|> pType <|> fnName

276281

277282cmd_consolewidth :: String -> P.IdrisParser (Either String Command)

278283cmd_consolewidth name = do