155e306 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fixed IdrisDoc errors and added REPL :help descriptions

155e306Philip Rasmussen13 years ago

src/Idris/Help.hs+3

compare with master

unifiedsplit

@@ -29,6 +29,9 @@ help =

29 ([":t"], ExprArg, "Check the type of an expression"),

30 ([":miss", ":missing"], NameArg, "Show missing clauses"),

31 ([":doc"], NameArg, "Show internal documentation"),

32+ ([":mkdoc"], NoArg, "Generate IdrisDoc for all .idr files in working directory and subdirectories"),

33+ ([":mkdoc"], NameArg, "Generate IdrisDoc for target namespace"),

34+ ([":mkdoc"], OptionArg, "Generate IdrisDoc. Options: [notrace] [ns | dir] [TARGET]"),

32 ([":apropos"], NoArg, "Search names, types, and documentation"),

35 ([":apropos"], NoArg, "Search names, types, and documentation"),

33 ([":i", ":info"], NameArg, "Display information about a type class"),

36 ([":i", ":info"], NameArg, "Display information about a type class"),

34 ([":total"], NameArg, "Check the totality of a name"),

37 ([":total"], NameArg, "Check the totality of a name"),

src/Idris/IdrisDoc.hs+13−7

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

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

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

3import Idris.AbsSyntax (IState)

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

6type Failable = Either String

5type Failable = Either String

@@ -9,13 +8,20 @@ type Failable = Either String

9-- t: What do generate documentation for

8-- t: What do generate documentation for

10-- ot: Where to output documentation

9-- ot: Where to output documentation

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

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

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

11+generateDocs :: IState -> DocTarget -> FilePath -> Bool -> IO (Either String ())

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

12+generateDocs ist t ot trm = err "IdrisDoc has not been implemented yet..."

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

14+err :: String -> IO (Failable ())

16−error s = return Left s

15+err s = return $ Left s

18-- Target to generate documentation for

17-- Target to generate documentation for

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

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

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

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

21−data DocTarget = Namespace String | Dir FilePath

20+data DocTarget = Namespace String | Dir FilePath

21+

22+idrisDocUsage = "Usage: :mkdoc [notrace] [ns | dir] [TARGET]\n\n" ++

23+ "notrace: Do not generate IdrisDoc for addtionally referred namespaces.\n" ++

24+ "ns: TARGET is a loaded namespace. TARGET required.\n" ++

25+ "dir: TARGET is a directory to search recursively for .idr files. TARGET required.\n" ++

26+ "TARGET: What to generate IdrisDoc for. By default interpreted as a namespace.\n" ++

27+ "<none>: Same as ':mkdoc dir .'"

src/Idris/REPL.hs+13−14

@@ -978,21 +978,20 @@ process h fn (Apropos a) =

978

979-- IdrisDoc

980process h fn (MakeDoc s) =

981− do istate <- getIState

981+ do istate <- getIState

982− outputTarget <- runIO $ getCurrentDirectory

982+ outputTarget <- runIO $ getCurrentDirectory

983− let trim = dropWhile isSpace

983+ let trim = dropWhile isSpace

984− s' = trim s

984+ s' = trim s

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

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

986− Nothing -> (True, s')

986+ Nothing -> (True, s')

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

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

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

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

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

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

990− else if null s'' then Dir outputTarget

990+ else if null s'' then Dir outputTarget

991− else Namespace (s'')

991+ else Namespace (s'')

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

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

994+ Left err -> iPrintError (err ++ "\n" ++ idrisDocUsage)

996

995

997classInfo :: ClassInfo -> Idris ()

996classInfo :: ClassInfo -> Idris ()

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

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