877c638 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

IdrisDoc begun

commit877c6389b590a274a9ae866b8af5d9563a6925f1 authorPhilip Rasmussen <pjor@itu.dk> dateMon 24 Mar 2014, 21:58 (13 years ago) parent9c99a07

5 files changed+43

compare with master

unifiedsplit

idris.cabal+1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/IdrisDoc.hs+21 src/Idris/REPL.hs+19 src/Idris/REPLParser.hs+1

idris.cabal+1

@@ -474,6 +474,7 @@ Library

474474 , Idris.Help

475475 , Idris.IBC

476476 , Idris.IdeSlave

477+ , Idris.IdrisDoc

477478 , Idris.Imports

478479 , Idris.Inliner

479480 , Idris.Parser

src/Idris/AbsSyntaxTree.hs+1

@@ -293,6 +293,7 @@ data Command = Quit

293293 | ListErrorHandlers

294294 | SetConsoleWidth ConsoleWidth

295295 | Apropos String

296+ | MakeDoc String -- IdrisDoc

296297

297298data Opt = Filename String

298299 | Ver

src/Idris/IdrisDoc.hsnew file+21

@@ -0,0 +1,21 @@

1+module Idris.IdrisDoc (generateDocs, DocTarget) where

3+import Idris.AbsSyntax (IState)

4+import Idris.Core.TT (Err')

6+type Failable = Either String

8+-- ist: IState

9+-- t: What do generate documentation for

10+-- ot: Where to output documentation

11+-- trm: Trace mode? (will generate documentation for referred modules)

12+generateDocs :: IState -> DocTarget -> Filepath -> Bool -> IO (Either String ())

13+generateDocs ist t ot trm = error "IdrisDoc has not been implemented yet..."

14+

15+error :: String -> IO (Failable ())

16+error s = return Left s

17+

18+-- Target to generate documentation for

19+-- Namespace ns: Generate documentation for the namespace identified by 'ns'

20+-- Dir d: Generate documentation for all namespaces in the directory 'd'

21+data DocTarget = Namespace String | Dir FilePath

src/Idris/REPL.hs+19

@@ -12,6 +12,7 @@ import Idris.Error

1212import Idris.ErrReverse

1313import Idris.Delaborate

1414import Idris.Docstrings (Docstring, overview, renderDocstring)

15+import Idris.IdrisDoc

1516import Idris.Prover

1617import Idris.Parser

1718import Idris.Primitives

@@ -975,6 +976,24 @@ process h fn (Apropos a) =

975976 isUN (NS n _) = isUN n

976977 isUN _ = False

977978

979+-- IdrisDoc

980+process h fn (MakeDoc s) =

981+ do istate <- getIState

982+ outputTarget <- runIO $ getCurrentDirectory

983+ let trim = dropWhile isSpace

984+ s' = trim s

985+ (trace, s'') = case (stripPrefix "notrace" s') of Just x -> (False, trim x)

986+ Nothing -> (True, s')

987+ target = let (front, back) = span (not . isSpace) s''

988+ in if front == "ns" then Namespace (trim back)

989+ else if front == "dir" then Dir (trim back)

990+ else if null s'' then Dir outputTarget

991+ else Namespace (s'')

992+ result <- runIO $ generateDocs istate target outputTarget trace

993+ case result of Right _ -> iputStrLn "IdrisDoc generated"

994+ Left err -> let u = "Usage: :mkdoc [notrace] [ns | dir] [TARGET]"

995+ in iPrintError err ++ "\n" ++ u

996+

978997classInfo :: ClassInfo -> Idris ()

979998classInfo ci = do iputStrLn "Methods:\n"

980999 mapM_ dumpMethod (class_methods ci)

src/Idris/REPLParser.hs+1

@@ -99,6 +99,7 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

9999 <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

100100 <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

101101 <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))

102+ <|> try (do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)) -- IdrisDoc

102103 <|> do P.whiteSpace; do eof; return NOP

103104 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

104105