@@ -10,6 +10,7 @@ import Idris.Delaborate
1010import Idris.Compiler
1111import Idris.Prover
1212import Idris.Parser
13+import Paths_miniidris
1314
1415import Core.Evaluate
1516import Core.ProofShell
@@ -23,6 +24,7 @@ import Control.Monad
2324import Control.Monad.State
2425import Data.List
2526import Data.Char
27+import Data.Version
2628
2729repl :: IState -> [FilePath] -> Idris ()
2830repl orig mods
@@ -60,8 +62,7 @@ processInput cmd orig inputs
6062 return (Just inputs)
6163
6264process :: FilePath -> Command -> Idris ()
63−process _ Help
64− = iputStrLn "At some point I'll write some help text. Thanks for asking though."
65+process _ Help = iputStrLn displayHelp
6566process "" Edit = iputStrLn "Nothing to edit"
6667process f Edit
6768 = do i <- get
@@ -108,3 +109,25 @@ process _ Metavars = do ist <- get
108109 _ -> iputStrLn $ "Global metavariables:\n\t" ++ show mvs
109110process _ NOP = return ()
110111
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
117+ col c1 c2 l m r =
118+ l ++ take (c1 - length l) (repeat ' ') ++
119+ m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
120+
121+help =
122+ [ (["Command"], "Arguments", "Purpose"),
123+ ([""], "", ""),
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")
132+ ]
133+