@@ -10,6 +10,7 @@ import Idris.Delaborate
10import Idris.Compiler
10import Idris.Compiler
11import Idris.Prover
11import Idris.Prover
12import Idris.Parser
12import Idris.Parser
13+import Paths_miniidris
14import Core.Evaluate
15import Core.Evaluate
15import Core.ProofShell
16import Core.ProofShell
@@ -23,6 +24,7 @@ import Control.Monad
23import Control.Monad.State
24import Control.Monad.State
24import Data.List
25import Data.List
25import Data.Char
26import Data.Char
27repl :: IState -> [FilePath] -> Idris ()
29repl :: IState -> [FilePath] -> Idris ()
28repl orig mods
30repl orig mods
@@ -60,8 +62,7 @@ processInput cmd orig inputs
60 return (Just inputs)
62 return (Just inputs)
62process :: FilePath -> Command -> Idris ()
64process :: FilePath -> Command -> Idris ()
63−process _ Help
65+process _ Help = iputStrLn displayHelp
64− = iputStrLn "At some point I'll write some help text. Thanks for asking though."
65process "" Edit = iputStrLn "Nothing to edit"
66process "" Edit = iputStrLn "Nothing to edit"
66process f Edit
67process f Edit
67 = do i <- get
68 = do i <- get
@@ -108,3 +109,25 @@ process _ Metavars = do ist <- get
108 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
109 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
109process _ NOP = return ()
110process _ NOP = return ()
112+displayHelp = let vstr = showVersion version in
113+ "\nIdris version " ++ vstr ++ "\n" ++
114+ "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
115+ concatMap cmdInfo help
116+ where cmdInfo (cmds, args, text) = " " ++ col 14 14 (showSep " " cmds) args text
118+ l ++ take (c1 - length l) (repeat ' ') ++
119+ m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
122+ [ (["Command"], "Arguments", "Purpose"),
124+ (["<expression>"], "", "Evaluate an expression"),
125+ ([":r",":reload"], "", "Reload current file"),
126+ ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
127+ ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
128+ ([":p",":prove"], "<name>", "Prove a metavariable"),
129+ ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
130+ ([":?",":h",":help"], "", "Display this help text"),
131+ ([":q",":quit"], "", "Exit the Idris system")