git.iko.soy/Idris-dev
on f92ecd2 help sign in
Idris-dev/src/Idris/Help.hs
60 lines 3.4 kB history raw
1{-|
2Module : Idris.Help
3Description : Utilities to aid with the REPL's HELP system.
5License : BSD3
6Maintainer : The Idris Community.
7-}
9module Idris.Help (CmdArg(..), extraHelp) where
11data CmdArg = ExprArg -- ^ The command takes an expression
12 | NameArg -- ^ The command takes a name
13 | FileArg -- ^ The command takes a file
14 | ShellCommandArg -- ^ The command takes a shell command name
15 | ModuleArg -- ^ The command takes a module name
16 | PkgArgs -- ^ The command takes a list of package names
17 | NumberArg -- ^ The command takes a number
18 | NamespaceArg -- ^ The command takes a namespace name
19 | OptionArg -- ^ The command takes an option
20 | MetaVarArg -- ^ The command takes a metavariable
21 | ColourArg -- ^ The command is the colour-setting command
22 | NoArg -- ^ No completion (yet!?)
23 | SpecialHeaderArg -- ^ do not use
24 | ConsoleWidthArg -- ^ The width of the console
25 | DeclArg -- ^ An Idris declaration, as might be contained in a file
26 | ManyArgs CmdArg -- ^ Zero or more of one kind of argument
27 | OptionalArg CmdArg -- ^ Zero or one of one kind of argument
28 | SeqArgs CmdArg CmdArg -- ^ One kind of argument followed by another
30instance Show CmdArg where
31 show ExprArg = "<expr>"
32 show NameArg = "<name>"
33 show FileArg = "<filename>"
34 show ShellCommandArg = "<command>"
35 show ModuleArg = "<module>"
36 show PkgArgs = "<package list>"
37 show NumberArg = "<number>"
38 show NamespaceArg = "<namespace>"
39 show OptionArg = "<option>"
40 show MetaVarArg = "<hole>"
41 show ColourArg = "<option>"
42 show NoArg = ""
43 show SpecialHeaderArg = "Arguments"
44 show ConsoleWidthArg = "auto|infinite|<number>"
45 show DeclArg = "<top-level declaration>"
46 show (ManyArgs a) = "(" ++ show a ++ ")..."
47 show (OptionalArg a) = "[" ++ show a ++ "]"
48 show (SeqArgs a b) = show a ++ " " ++ show b
50-- | Use these for completion, but don't show them in :help
51extraHelp ::[([String], CmdArg, String)]
52extraHelp =
53 [ ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")
54 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")
55 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")
56 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")
57 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")
58 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")
59 , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing holes for arguments that aren't inferrable")
60 ]