@@ -27,106 +27,107 @@ parseCmd :: IState -> String -> String -> Result Command
2727parseCmd i inputname = P.runparser pCmd i inputname
2828
2929cmd :: [String] -> P.IdrisParser ()
30−cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
30+cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs))
3131 where docmd [] = fail "No such command"
32− docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs
32+ docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs
3333
3434pCmd :: P.IdrisParser Command
35−pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)
36− <|> try (do cmd ["h", "?", "help"]; eof; return Help)
37− <|> try (do cmd ["w", "warranty"]; eof; return Warranty)
38− <|> try (do cmd ["r", "reload"]; eof; return Reload)
39− <|> try (do cmd ["module"]; f <- P.identifier; eof;
40− return (ModImport (toPath f)))
41− <|> try (do cmd ["e", "edit"]; eof; return Edit)
42− <|> try (do cmd ["exec", "execute"]; eof; return Execute)
43− <|> try (do cmd ["c", "compile"]
44− i <- get
45− c <- option (opt_codegen $ idris_options i) codegenOption
46− f <- P.identifier
47− eof
48− return (Compile c f))
49− <|> try (do cmd ["proofs"]; eof; return Proofs)
50− <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))
51− <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))
52− <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))
53− <|> try (do cmd ["let"]
54− defn <- concat <$> many (P.decl defaultSyntax)
55− return (NewDefn defn))
56− <|> try (do cmd ["unlet","undefine"]
57− Undefine `fmap` many P.name)
58− <|> try (do cmd ["lto", "loadto"];
59− toline <- P.natural
60− f <- many anyChar;
61− return (Load f (Just (fromInteger toline))))
62− <|> try (do cmd ["l", "load"]; f <- many anyChar;
63− return (Load f Nothing))
64− <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))
65− <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))
66− <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))
67− <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))
68− <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))
69− <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))
70− <|> try (do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n))
71− <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))
72− <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))
73− <|> try (do cmd ["u", "universes"]; eof; return Universes)
74− <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))
75− <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))
35+
36+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit
37+ <|> do cmd ["h", "?", "help"]; eof; return Help
38+ <|> do cmd ["w", "warranty"]; eof; return Warranty
39+ <|> do cmd ["r", "reload"]; eof; return Reload
40+ <|> do cmd ["module"]; f <- P.identifier; eof;
41+ return (ModImport (toPath f))
42+ <|> do cmd ["e", "edit"]; eof; return Edit
43+ <|> do cmd ["exec", "execute"]; eof; return Execute
44+ <|> do cmd ["c", "compile"]
45+ i <- get
46+ c <- option (opt_codegen $ idris_options i) codegenOption
47+ f <- P.identifier
48+ eof
49+ return (Compile c f)
50+ <|> do cmd ["proofs"]; eof; return Proofs
51+ <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)
52+ <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)
53+ <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))
54+ <|> do cmd ["let"]
55+ defn <- concat <$> many (P.decl defaultSyntax)
56+ return (NewDefn defn)
57+ <|> do cmd ["unlet","undefine"]
58+ Undefine `fmap` many P.name
59+ <|> do cmd ["lto", "loadto"];
60+ toline <- P.natural
61+ f <- many anyChar;
62+ return (Load f (Just (fromInteger toline)))
63+ <|> do cmd ["l", "load"]; f <- many anyChar;
64+ return (Load f Nothing)
65+ <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)
66+ <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)
67+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)
68+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)
69+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))
70+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))
71+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)
72+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)
73+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)
74+ <|> do cmd ["u", "universes"]; eof; return Universes
75+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)
76+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)
7677 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
77− <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))
78− <|> try (do cmd ["color", "colour"]; pSetColourCmd)
79− <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))
80− <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))
81− <|> try (do cmd ["s", "search"]; P.whiteSpace;
82− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))
83− <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;
84− upd <- option False (do P.lchar '!'; return True)
85− l <- P.natural; n <- P.name;
86− return (CaseSplitAt upd (fromInteger l) n))
87− <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;
88− upd <- option False (do P.lchar '!'; return True)
89− l <- P.natural; n <- P.name;
90− return (AddProofClauseFrom upd (fromInteger l) n))
91− <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;
92− upd <- option False (do P.lchar '!'; return True)
93− l <- P.natural; n <- P.name;
94− return (AddClauseFrom upd (fromInteger l) n))
95− <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;
96− upd <- option False (do P.lchar '!'; return True)
97− l <- P.natural; n <- P.name;
98− return (AddMissing upd (fromInteger l) n))
99− <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;
100− upd <- option False (do P.lchar '!'; return True)
101− l <- P.natural; n <- P.name;
102− return (MakeWith upd (fromInteger l) n))
103− <|> try (do cmd ["ml", "makelemma"]; P.whiteSpace;
104− upd <- option False (do P.lchar '!'; return True)
105− l <- P.natural; n <- P.name;
106− return (MakeLemma upd (fromInteger l) n))
107− <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;
108− upd <- option False (do P.lchar '!'; return True)
109− l <- P.natural; n <- P.name;
110− hints <- many P.fnName
111− return (DoProofSearch upd True (fromInteger l) n hints))
112− <|> try (do cmd ["ref", "refine"]; P.whiteSpace;
113− upd <- option False (do P.lchar '!'; return True)
114− l <- P.natural; n <- P.name;
115− hint <- P.fnName
116− return (DoProofSearch upd False (fromInteger l) n [hint]))
117− <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))
118− <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
119− <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;
120− return (Just x))
121− eof; return (AddProof n))
122− <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))
123− <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))
124− <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)
125− <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))
126− <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))
127− <|> try (do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n))
128− <|> try (do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n))
129− <|> try (do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str))
78+ <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)
79+ <|> do cmd ["color", "colour"]; pSetColourCmd
80+ <|> do cmd ["set"]; o <- pOption; return (SetOpt o)
81+ <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)
82+ <|> do cmd ["s", "search"]; P.whiteSpace;
83+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)
84+ <|> do cmd ["cs", "casesplit"]; P.whiteSpace;
85+ upd <- option False (do P.lchar '!'; return True)
86+ l <- P.natural; n <- P.name;
87+ return (CaseSplitAt upd (fromInteger l) n)
88+ <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;
89+ upd <- option False (do P.lchar '!'; return True)
90+ l <- P.natural; n <- P.name;
91+ return (AddProofClauseFrom upd (fromInteger l) n)
92+ <|> do cmd ["ac", "addclause"]; P.whiteSpace;
93+ upd <- option False (do P.lchar '!'; return True)
94+ l <- P.natural; n <- P.name;
95+ return (AddClauseFrom upd (fromInteger l) n)
96+ <|> do cmd ["am", "addmissing"]; P.whiteSpace;
97+ upd <- option False (do P.lchar '!'; return True)
98+ l <- P.natural; n <- P.name;
99+ return (AddMissing upd (fromInteger l) n)
100+ <|> do cmd ["mw", "makewith"]; P.whiteSpace;
101+ upd <- option False (do P.lchar '!'; return True)
102+ l <- P.natural; n <- P.name;
103+ return (MakeWith upd (fromInteger l) n)
104+ <|> do cmd ["ml", "makelemma"]; P.whiteSpace;
105+ upd <- option False (do P.lchar '!'; return True)
106+ l <- P.natural; n <- P.name;
107+ return (MakeLemma upd (fromInteger l) n)
108+ <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;
109+ upd <- option False (do P.lchar '!'; return True)
110+ l <- P.natural; n <- P.name;
111+ hints <- many P.fnName
112+ return (DoProofSearch upd True (fromInteger l) n hints)
113+ <|> do cmd ["ref", "refine"]; P.whiteSpace;
114+ upd <- option False (do P.lchar '!'; return True)
115+ l <- P.natural; n <- P.name;
116+ hint <- P.fnName
117+ return (DoProofSearch upd False (fromInteger l) n [hint])
118+ <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)
119+ <|> do cmd ["m", "metavars"]; eof; return Metavars
120+ <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;
121+ return (Just x))
122+ eof; return (AddProof n)
123+ <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)
124+ <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)
125+ <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers
126+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)
127+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)
128+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)
129+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)
130+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)
130131 <|> do P.whiteSpace; do eof; return NOP
131132 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
132133