3643346 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+2−2

compare with master

unifiedsplit

@@ -637,8 +637,8 @@ setWidth :: ConsoleWidth -> Idris ()

637setWidth w = do ist <- getIState

638 put ist { idris_consolewidth = w }

639

640−

640+typeDescription :: String

641−

641+typeDescription = "The type of types"

642

643type1Doc :: Doc OutputAnnotation

644type1Doc = (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, pprintType1Doc, 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+pprintType1Doc :: IState -> Doc OutputAnnotation

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

324+ nest 4 (line <> text typeDescription)

src/Idris/REPL.hs+15−13

@@ -942,19 +942,21 @@ process fn (Core t)

942

943process fn (DocStr (Left n) w)

944 = do ist <- getIState

945+ case show n of

946+ "Type" -> iRenderResult $ pprintType1Doc ist

945− let docs = lookupCtxtName n (idris_docstrings ist) ++

947+ _ -> do let docs = lookupCtxtName n (idris_docstrings ist) ++

946− map (\(n,d)-> (n, (d, [])))

948+ map (\(n,d)-> (n, (d, [])))

947− (lookupCtxtName (modDocN n) (idris_moduledocs ist))

949+ (lookupCtxtName (modDocN n) (idris_moduledocs ist))

948− case docs of

950+ case docs of

949− [] -> iPrintError $ "No documentation for " ++ show n

951+ [] -> iPrintError $ "No documentation for " ++ show n

950− ns -> do toShow <- mapM (showDoc ist) ns

952+ ns -> do toShow <- mapM (showDoc ist) ns

951− iRenderResult (vsep toShow)

953+ iRenderResult (vsep toShow)

952− where showDoc ist (n, d) = do doc <- getDocs n w

954+ where showDoc ist (n, d) = do doc <- getDocs n w

953− return $ pprintDocs ist doc

955+ return $ pprintDocs ist doc

954−

956+

955− modDocN (NS (UN n) ns) = NS modDocName (n:ns)

957+ modDocN (NS (UN n) ns) = NS modDocName (n:ns)

956− modDocN (UN n) = NS modDocName [n]

958+ modDocN (UN n) = NS modDocName [n]

957− modDocN _ = sMN 1 "NotFoundForSure"

959+ modDocN _ = sMN 1 "NotFoundForSure"

958

960

959process fn (DocStr (Right c) _) -- constants only have overviews

961process fn (DocStr (Right c) _) -- constants only have overviews

960 = do ist <- getIState

962 = do ist <- getIState

src/Idris/REPLParser.hs+6−1

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

268 c <- fmap fst P.constant

269 eof

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

271+

272+ let pType = do

273+ P.reserved "Type"

274+ eof

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

271

276

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

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

273

278

274− try constant <|> fnName

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

275

280

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

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

277cmd_consolewidth name = do

282cmd_consolewidth name = do