3643346 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed REPL for `:doc Type` to display documentation rather than an error

message

commit3643346a16ba9facf4c708784f6db5bee0586a3c authorRossMeikleham <rossmeikleham@hotmail.co.uk> dateFri 29 May 2015, 12:07 (11 years ago) parent0c953a9

4 files changed+29−17

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−2 src/Idris/Docs.hs+6−1 src/Idris/REPL.hs+15−13 src/Idris/REPLParser.hs+6−1

src/Idris/AbsSyntax.hs+2−2

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

637637setWidth w = do ist <- getIState

638638 put ist { idris_consolewidth = w }

639639

640−

641−

640+typeDescription :: String

641+typeDescription = "The type of types"

642642

643643type1Doc :: Doc OutputAnnotation

644644type1Doc = (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, pprintType1Doc, 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+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)

942942

943943process fn (DocStr (Left n) w)

944944 = do ist <- getIState

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

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

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

948− case docs of

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

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

951− iRenderResult (vsep toShow)

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

953− return $ pprintDocs ist doc

954−

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

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

957− modDocN _ = sMN 1 "NotFoundForSure"

945+ case show n of

946+ "Type" -> iRenderResult $ pprintType1Doc ist

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

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

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

950+ case docs of

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

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

953+ iRenderResult (vsep toShow)

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

955+ return $ pprintDocs ist doc

956+

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

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

959+ modDocN _ = sMN 1 "NotFoundForSure"

958960

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

960962 = do ist <- getIState

src/Idris/REPLParser.hs+6−1

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

268268 c <- fmap fst P.constant

269269 eof

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

271276

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

273278

274− try constant <|> fnName

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

275280

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

277282cmd_consolewidth name = do