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