diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index fafc526..5e69248 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1533,6 +1533,8 @@ nonEmptyCommand <|> do symbol ":"; exactIdent "exec" tm <- expr pdef "(interactive)" init pure (Exec tm) + <|> do symbol ":"; replCmd ["?", "h", "help"] + pure Help <|> do symbol ":"; replCmd ["r", "reload"] pure Reload <|> do symbol ":"; replCmd ["e", "edit"] diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 656f4b0..64284d0 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -456,6 +456,7 @@ data REPLResult : Type where Done : REPLResult REPLError : String -> REPLResult Executed : PTerm -> REPLResult + RequestedHelp : REPLResult Evaluated : PTerm -> (Maybe PTerm) -> REPLResult Printed : List String -> REPLResult TermChecked : PTerm -> PTerm -> REPLResult @@ -620,6 +621,8 @@ process (Compile ctm outfile) = compileExp ctm outfile process (Exec ctm) = execExp ctm +process Help + = pure RequestedHelp process (ProofSearch n_in) = do defs <- get Ctxt [(n, i, ty)] <- lookupTyName n_in (gamma defs) @@ -829,6 +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 (Edited (DisplayEdit [])) = pure () displayResult (Edited (DisplayEdit xs)) = printResult $ showSep "\n" xs displayResult (Edited (EditError x)) = printError x diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index df46e40..793a1b2 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -304,6 +304,7 @@ data REPLCmd : Type where Edit : REPLCmd Compile : PTerm -> String -> REPLCmd Exec : PTerm -> REPLCmd + Help : REPLCmd ProofSearch : Name -> REPLCmd DebugInfo : Name -> REPLCmd SetOpt : REPLOpt -> REPLCmd