@@ -27,72 +27,72 @@ parseCmd :: IState -> String -> String -> Result (Either String Command)
2727parseCmd i inputname = P.runparser pCmd i inputname
2828
2929pCmd :: P.IdrisParser (Either String Command)
30−pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit
31− <|> do c <- cmd ["h", "?", "help"]; noArgs c Help
32− <|> do c <- cmd ["w", "warranty"]; noArgs c Warranty
33− <|> do c <- cmd ["r", "reload"]; noArgs c Reload
34− <|> do c <- cmd ["exec", "execute"]; noArgs c Execute
35− <|> do c <- cmd ["proofs"]; noArgs c Proofs
36− <|> do c <- cmd ["u", "universes"]; noArgs c Universes
37− <|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
38− <|> do c <- cmd ["m", "metavars"]; noArgs c Metavars
39− <|> do c <- cmd ["e", "edit"]; noArgs c Edit
40−
41− <|> do c <- cmd ["d", "def"]; fnNameArg c Defn
42− <|> do c <- cmd ["total"]; fnNameArg c TotCheck
43− <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef
44− <|> do c <- cmd ["transinfo"]; fnNameArg c TransformInfo
45− <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
46− <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
47− <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
48− <|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing
49−
50− <|> do c <- cmd ["t", "type"]; exprArg c Check
51− <|> do c <- cmd ["x"]; exprArg c ExecVal
52− <|> do c <- cmd ["patt"]; exprArg c Pattelab
53− <|> do c <- cmd ["spec"]; exprArg c Spec
54− <|> do c <- cmd ["hnf"]; exprArg c HNF
55− <|> do c <- cmd ["inline"]; exprArg c TestInline
56−
57− <|> do c <- cmd ["rmproof"]; nameArg c RmProof
58− <|> do c <- cmd ["showproof"]; nameArg c ShowProof
59− <|> do c <- cmd ["p", "prove"]; nameArg c Prove
60−
61− <|> do c <- cmd ["set"]; optArg c SetOpt
62− <|> do c <- cmd ["unset"]; optArg c UnsetOpt
63−
64− <|> do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
65− <|> do c <- cmd ["cd"]; strArg c ChangeDirectory
66− <|> do c <- cmd ["apropos"]; strArg c Apropos
67− <|> do c <- cmd ["mkdoc"]; strArg c MakeDoc
68−
69− <|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
70− <|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
71− <|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
72− <|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
73− <|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
74− <|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
75−
76− <|> do c <- cmd ["pp", "pprint"]; cmd_pprint c
77− <|> do c <- cmd ["doc"]; cmd_doc c
78− <|> do c <- cmd ["dynamic"]; cmd_dynamic c
79− <|> do c <- cmd ["consolewidth"]; cmd_consolewidth c
80− <|> do c <- cmd ["module"]; cmd_module c
81− <|> do c <- cmd ["c", "compile"]; cmd_compile c
82− <|> do c <- cmd ["a", "addproof"]; cmd_addproof c
83− <|> do c <- cmd ["log"]; cmd_log c
84− <|> do c <- cmd ["let"]; cmd_let c
85− <|> do c <- cmd ["unlet","undefine"]; cmd_unlet c
86− <|> do c <- cmd ["lto", "loadto"]; cmd_loadto c
87− <|> do c <- cmd ["color", "colour"]; cmd_colour c
88− <|> do c <- cmd ["s", "search"]; cmd_search c
89− <|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
90− <|> do c <- cmd ["ref", "refine"]; cmd_refine c
91−
92− <|> unrecognized
93− <|> nop
94− <|> eval
95−
30+pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit
31+ , do c <- cmd ["h", "?", "help"]; noArgs c Help
32+ , do c <- cmd ["w", "warranty"]; noArgs c Warranty
33+ , do c <- cmd ["r", "reload"]; noArgs c Reload
34+ , do c <- cmd ["exec", "execute"]; noArgs c Execute
35+ , do c <- cmd ["proofs"]; noArgs c Proofs
36+ , do c <- cmd ["u", "universes"]; noArgs c Universes
37+ , do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
38+ , do c <- cmd ["m", "metavars"]; noArgs c Metavars
39+ , do c <- cmd ["e", "edit"]; noArgs c Edit
40+
41+ , do c <- cmd ["d", "def"]; fnNameArg c Defn
42+ , do c <- cmd ["total"]; fnNameArg c TotCheck
43+ , do c <- cmd ["printdef"]; fnNameArg c PrintDef
44+ , do c <- cmd ["transinfo"]; fnNameArg c TransformInfo
45+ , do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
46+ , do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
47+ , do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
48+ , do c <- cmd ["miss", "missing"]; fnNameArg c Missing
49+
50+ , do c <- cmd ["t", "type"]; exprArg c Check
51+ , do c <- cmd ["x"]; exprArg c ExecVal
52+ , do c <- cmd ["patt"]; exprArg c Pattelab
53+ , do c <- cmd ["spec"]; exprArg c Spec
54+ , do c <- cmd ["hnf"]; exprArg c HNF
55+ , do c <- cmd ["inline"]; exprArg c TestInline
56+
57+ , do c <- cmd ["rmproof"]; nameArg c RmProof
58+ , do c <- cmd ["showproof"]; nameArg c ShowProof
59+ , do c <- cmd ["p", "prove"]; nameArg c Prove
60+
61+ , do c <- cmd ["set"]; optArg c SetOpt
62+ , do c <- cmd ["unset"]; optArg c UnsetOpt
63+
64+ , do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
65+ , do c <- cmd ["cd"]; strArg c ChangeDirectory
66+ , do c <- cmd ["apropos"]; strArg c Apropos
67+ , do c <- cmd ["mkdoc"]; strArg c MakeDoc
68+
69+ , do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
70+ , do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
71+ , do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
72+ , do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
73+ , do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
74+ , do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
75+
76+ , do c <- cmd ["pp", "pprint"]; cmd_pprint c
77+ , do c <- cmd ["doc"]; cmd_doc c
78+ , do c <- cmd ["dynamic"]; cmd_dynamic c
79+ , do c <- cmd ["consolewidth"]; cmd_consolewidth c
80+ , do c <- cmd ["module"]; cmd_module c
81+ , do c <- cmd ["c", "compile"]; cmd_compile c
82+ , do c <- cmd ["a", "addproof"]; cmd_addproof c
83+ , do c <- cmd ["log"]; cmd_log c
84+ , do c <- cmd ["let"]; cmd_let c
85+ , do c <- cmd ["unlet","undefine"]; cmd_unlet c
86+ , do c <- cmd ["lto", "loadto"]; cmd_loadto c
87+ , do c <- cmd ["color", "colour"]; cmd_colour c
88+ , do c <- cmd ["s", "search"]; cmd_search c
89+ , do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
90+ , do c <- cmd ["ref", "refine"]; cmd_refine c
91+
92+ , unrecognized
93+ , nop
94+ ]
95+ <|> eval
9696 where nop = do P.whiteSpace; eof; return (Right NOP)
9797 eval = exprArg "" Eval
9898 unrecognized = do