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

src/Idris/AbsSyntax.hs+3

compare with master

unifiedsplit

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

641setDepth d = do ist <- getIState

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

643

644+typeDescription :: String

645+typeDescription = "The type of types"

646+

644

647

645type1Doc :: Doc OutputAnnotation

648type1Doc :: Doc OutputAnnotation

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

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

src/Idris/Docs.hs+6−1

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

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

2{-# 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

4

5import Idris.AbsSyntax

6import Idris.AbsSyntaxTree

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

317 t (Str _) = PConstant NoFC StrType

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

319 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)

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

946

947process fn (DocStr (Left n) w)

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

949+ | otherwise = do

948− = do ist <- getIState

950+ ist <- getIState

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

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

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

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

951 (lookupCtxtName (modDocN n) (idris_moduledocs ist))

953 (lookupCtxtName (modDocN n) (idris_moduledocs ist))

src/Idris/REPLParser.hs+6−1

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

269 c <- fmap fst P.constant

270 eof

271 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)

272

277

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

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

274

279

275− try constant <|> fnName

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

276

281

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

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

278cmd_consolewidth name = do

283cmd_consolewidth name = do