@@ -6,34 +6,44 @@ data CmdArg = ExprArg -- ^ The command takes an expression
66 | ModuleArg -- ^ The command takes a module name
77 | OptionArg -- ^ The command takes an option
88 | MetaVarArg -- ^ The command takes a metavariable
9− | NoArg -- ^ No completion yet
9+ | NoArg -- ^ No completion (yet!?)
10+ | SpecialHeaderArg -- ^ do not use
1011
11−-- TODO: Merge the second and fourth elements of the following tuples
12−help :: [([String], String, String, CmdArg)]
12+instance Show CmdArg where
13+ show ExprArg = "<expr>"
14+ show NameArg = "<name>"
15+ show FileArg = "<filename>"
16+ show ModuleArg = "<module>"
17+ show OptionArg = "<option>"
18+ show MetaVarArg = "<metavar>"
19+ show NoArg = ""
20+ show SpecialHeaderArg = "Arguments"
21+
22+help :: [([String], CmdArg, String)]
1323help =
14− [ (["<expr>"], "", "Evaluate an expression", NoArg),
15− ([":t"], "<expr>", "Check the type of an expression", ExprArg),
16− ([":miss", ":missing"], "<name>", "Show missing clauses", NameArg),
17− ([":i", ":info"], "<name>", "Display information about a type class", NameArg),
18− ([":total"], "<name>", "Check the totality of a name", NameArg),
19− ([":r",":reload"], "", "Reload current file", NoArg),
20− ([":l",":load"], "<filename>", "Load a new file", FileArg),
21− ([":m",":module"], "<module>", "Import an extra module", ModuleArg), -- NOTE: dragons
22− ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL", NoArg),
23− ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)", MetaVarArg),
24− ([":p",":prove"], "<name>", "Prove a metavariable", MetaVarArg),
25− ([":a",":addproof"], "<name>", "Add proof to source file", NameArg),
26− ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),
27− ([":showproof"], "<name>", "Show proof", NameArg),
28− ([":proofs"], "", "Show available proofs", NoArg),
29− ([":x"], "<expr>", "Execute IO actions resulting from an expression using the interpreter", ExprArg),
30− ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),
31− ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),
32− ([":exec",":execute"], "", "Compile to an executable and run", NoArg),
33− ([":dynamic"], "<filename>", "Dynamically load a C library (similar to %dynamic)", FileArg),
34− ([":dynamic"], "", "List dynamically loaded C libraries", NoArg),
35− ([":?",":h",":help"], "", "Display this help text", NoArg),
36− ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),
37− ([":unset"], "<option>", "Unset an option", OptionArg),
38− ([":q",":quit"], "", "Exit the Idris system", NoArg)
24+ [ (["<expr>"], NoArg, "Evaluate an expression"),
25+ ([":t"], ExprArg, "Check the type of an expression"),
26+ ([":miss", ":missing"], NameArg, "Show missing clauses"),
27+ ([":i", ":info"], NameArg, "Display information about a type class"),
28+ ([":total"], NameArg, "Check the totality of a name"),
29+ ([":r",":reload"], NoArg, "Reload current file"),
30+ ([":l",":load"], FileArg, "Load a new file"),
31+ ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
32+ ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),
33+ ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),
34+ ([":p",":prove"], MetaVarArg, "Prove a metavariable"),
35+ ([":a",":addproof"], NameArg, "Add proof to source file"),
36+ ([":rmproof"], NameArg, "Remove proof from proof stack"),
37+ ([":showproof"], NameArg, "Show proof"),
38+ ([":proofs"], NoArg, "Show available proofs"),
39+ ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),
40+ ([":c",":compile"], FileArg, "Compile to an executable <filename>"),
41+ ([":js", ":javascript"], FileArg, "Compile to JavaScript <filename>"),
42+ ([":exec",":execute"], NoArg, "Compile to an executable and run"),
43+ ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),
44+ ([":dynamic"], NoArg, "List dynamically loaded C libraries"),
45+ ([":?",":h",":help"], NoArg, "Display this help text"),
46+ ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),
47+ ([":unset"], OptionArg, "Unset an option"),
48+ ([":q",":quit"], NoArg, "Exit the Idris system")
3949 ]