git.iko.soy/Idris-dev
on 20ffcfd help sign in
Idris-dev/src/Idris/Help.hs
71 lines 4.4 kB history raw
1module Idris.Help (CmdArg(..), help, extraHelp) 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 | ColourArg -- ^ The command is the colour-setting command
10 | NoArg -- ^ No completion (yet!?)
11 | SpecialHeaderArg -- ^ do not use
13instance Show CmdArg where
14 show ExprArg = "<expr>"
15 show NameArg = "<name>"
16 show FileArg = "<filename>"
17 show ModuleArg = "<module>"
18 show OptionArg = "<option>"
19 show MetaVarArg = "<metavar>"
20 show ColourArg = "<option>"
21 show NoArg = ""
22 show SpecialHeaderArg = "Arguments"
24help :: [([String], CmdArg, String)]
25help =
26 [ (["<expr>"], NoArg, "Evaluate an expression"),
27 ([":t"], ExprArg, "Check the type of an expression"),
28 ([":miss", ":missing"], NameArg, "Show missing clauses"),
29 ([":doc"], NameArg, "Show internal documentation"),
30 ([":i", ":info"], NameArg, "Display information about a type class"),
31 ([":total"], NameArg, "Check the totality of a name"),
32 ([":r",":reload"], NoArg, "Reload current file"),
33 ([":l",":load"], FileArg, "Load a new file"),
34 ([":cd"], FileArg, "Change working directory"),
35 ([":m",":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons
36 ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),
37 ([":m",":metavars"], MetaVarArg, "Show remaining proof obligations (metavariables)"),
38 ([":p",":prove"], MetaVarArg, "Prove a metavariable"),
39 ([":a",":addproof"], NameArg, "Add proof to source file"),
40 ([":rmproof"], NameArg, "Remove proof from proof stack"),
41 ([":showproof"], NameArg, "Show proof"),
42 ([":proofs"], NoArg, "Show available proofs"),
43 ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),
44 ([":c",":compile"], FileArg, "Compile to an executable <filename>"),
45 ([":js", ":javascript"], FileArg, "Compile to JavaScript <filename>"),
46 ([":exec",":execute"], NoArg, "Compile to an executable and run"),
47 ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),
48 ([":dynamic"], NoArg, "List dynamically loaded C libraries"),
49 ([":?",":h",":help"], NoArg, "Display this help text"),
50 ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),
51 ([":unset"], OptionArg, "Unset an option"),
52 ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),
53 ([":q",":quit"], NoArg, "Exit the Idris system")
54 ]
56-- | Use these for completion, but don't show them in :help
57extraHelp ::[([String], CmdArg, String)]
58extraHelp =
59 [ ([":casesplit", ":cs"], NoArg, ":cs <line> <name> splits the pattern variable on the line")
60 , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")
61 , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")
62 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")
63 , ([":addmissing", ":am"], NoArg, ":am <line> <name> adds all missing pattern matches for the name on the line")
64 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")
65 , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")
66 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")
67 , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")
68 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")
69 , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")
70 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")
71 ]