git.iko.soy/Idris-dev
on master help sign in
Fixed IdrisDoc errors and added REPL :help descriptions
commit155e306ef9982cddc56eaf9ae979a90fed022d05 authorPhilip Rasmussen <pjor@itu.dk> dateTue 25 Mar 2014, 13:39 (13 years ago) parent877c638
3 files changed+29−21
compare with master
unifiedsplit
src/Idris/Help.hs+3 src/Idris/IdrisDoc.hs+13−7 src/Idris/REPL.hs+13−14
src/Idris/Help.hs+3
@@ -29,6 +29,9 @@ help =
2929 ([":t"], ExprArg, "Check the type of an expression"),
3030 ([":miss", ":missing"], NameArg, "Show missing clauses"),
3131 ([":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]"),
3235 ([":apropos"], NoArg, "Search names, types, and documentation"),
3336 ([":i", ":info"], NameArg, "Display information about a type class"),
3437 ([":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
22
33import Idris.AbsSyntax (IState)
4−import Idris.Core.TT (Err')
54
65type Failable = Either String
76
@@ -9,13 +8,20 @@ type Failable = Either String
98-- t: What do generate documentation for
109-- ot: Where to output documentation
1110-- 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..."
11+generateDocs :: IState -> DocTarget -> FilePath -> Bool -> IO (Either String ())
12+generateDocs ist t ot trm = err "IdrisDoc has not been implemented yet..."
1413
15−error :: String -> IO (Failable ())
16−error s = return Left s
14+err :: String -> IO (Failable ())
15+err s = return $ Left s
1716
1817-- Target to generate documentation for
1918-- Namespace ns: Generate documentation for the namespace identified by 'ns'
2019-- 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) =
978978
979979-- IdrisDoc
980980process 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
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
993993 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)
996995
997996classInfo :: ClassInfo -> Idris ()
998997classInfo ci = do iputStrLn "Methods:\n"