git.iko.soy/Idris-dev
on dfbb3db help sign in
Idris-dev/src/Idris/Help.hs
50 lines 2.5 kB history raw
1module Idris.Help (CmdArg(..), help) where
3data CmdArg = ExprArg -- ^ The command takes an expression
4 | NameArg -- ^ The command takes a name
5 | FileArg -- ^ The command takes a file
6 | ModuleArg -- ^ The command takes a module name
7 | OptionArg -- ^ The command takes an option
8 | MetaVarArg -- ^ The command takes a metavariable
9 | NoArg -- ^ No completion (yet!?)
10 | SpecialHeaderArg -- ^ do not use
12instance 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"
22help :: [([String], CmdArg, String)]
23help =
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 ([":cd"], FileArg, "Change working directory"),
32 ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
33 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),
34 ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),
35 ([":p",":prove"], MetaVarArg, "Prove a metavariable"),
36 ([":a",":addproof"], NameArg, "Add proof to source file"),
37 ([":rmproof"], NameArg, "Remove proof from proof stack"),
38 ([":showproof"], NameArg, "Show proof"),
39 ([":proofs"], NoArg, "Show available proofs"),
40 ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),
41 ([":c",":compile"], FileArg, "Compile to an executable <filename>"),
42 ([":js", ":javascript"], FileArg, "Compile to JavaScript <filename>"),
43 ([":exec",":execute"], NoArg, "Compile to an executable and run"),
44 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),
45 ([":dynamic"], NoArg, "List dynamically loaded C libraries"),
46 ([":?",":h",":help"], NoArg, "Display this help text"),
47 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),
48 ([":unset"], OptionArg, "Unset an option"),
49 ([":q",":quit"], NoArg, "Exit the Idris system")
50 ]