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