Add ability to display the help

src/Idris/Parser.idr

@@ -1502,6 +1502,42 @@ editCmd
          pure (MakeWith upd (fromInteger line) n)
   <|> fatalError "Unrecognised command"
 
+export
+data CmdArg : Type where
+     ||| The command takes an expression.
+     ExprArg : CmdArg
+     NoArg : CmdArg
+
+export
+Show CmdArg where
+  show ExprArg = "<expr>"
+  show NoArg = ""
+
+CommandDefinition : Type
+CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
+
+CommandTable : Type
+CommandTable = List CommandDefinition
+
+exprArg : (PTerm -> REPLCmd) -> Rule REPLCmd
+exprArg command = do
+  tm <- expr pdef "(interactive)" init
+  pure (command tm)
+
+exprArgCmd : List String -> (PTerm -> REPLCmd) -> String -> CommandDefinition
+exprArgCmd names command doc =
+  (names, ExprArg, doc, exprArg command)
+
+parserCommandsForHelp : CommandTable
+parserCommandsForHelp =
+  [ exprArgCmd ["t", "type"] Check "Check the type of an expression"
+  ]
+
+export
+help : List (List String, CmdArg, String)
+help = (["<expr>"], NoArg, "Evaluate an expression") ::
+  [ (map (":" ++) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]
+
 nonEmptyCommand : Rule REPLCmd
 nonEmptyCommand
     = do symbol ":"; replCmd ["t", "type"]

src/Idris/REPL.idr

@@ -832,7 +832,7 @@ mutual
                                    showSep ", " (map show xs)
   displayResult  (LogLevelSet k) = printResult $ "Set loglevel to " ++ show k
   displayResult  (VersionIs x) = printResult $ showVersion True x
-  displayResult  (RequestedHelp) = printResult $ "This is where the help will go"
+  displayResult  (RequestedHelp) = printResult displayHelp
   displayResult  (Edited (DisplayEdit [])) = pure ()
   displayResult  (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs
   displayResult  (Edited (EditError x)) = printError x
@@ -840,6 +840,11 @@ mutual
   displayResult  (OptionsSet opts) = printResult $ showSep "\n" $ map show opts
   displayResult  _ = pure ()
 
+  displayHelp : String
+  displayHelp =
+    showSep "\n" $ map cmdInfo help
+    where cmdInfo (cmds, args, text) = "   " ++ showSep " " cmds ++ " " ++ show args ++ " " ++ text
+
   export
   displayErrors : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->