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