@@ -23,47 +23,47 @@ cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
2323 docmd (x:xs) = try (discard (symbol x)) <|> docmd xs
2424
2525pCmd :: IParser Command
26−pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
27− <|> try (do cmd ["h", "?", "help"]; eof; return Help)
28− <|> try (do cmd ["r", "reload"]; eof; return Reload)
29− <|> try (do cmd ["m", "module"]; f <- identifier; eof;
30− return (ModImport (toPath f)))
31− <|> try (do cmd ["e", "edit"]; eof; return Edit)
32− <|> try (do cmd ["exec", "execute"]; eof; return Execute)
33− <|> try (do cmd ["ttshell"]; eof; return TTShell)
34− <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
35− <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
36− <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))
37− <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
38− <|> try (do cmd ["proofs"]; eof; return Proofs)
39− <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
40− <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;
41− return (Just x))
42− eof; return (AddProof n))
43− <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
44− <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
45− <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
46− <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))
47− <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))
48− <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
49− <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
50− <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))
51− <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))
52− <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
53− <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))
54− <|> try (do cmd ["u", "universes"]; eof; return Universes)
55− <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
56− <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
57− <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))
58− <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
59− <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))
60− <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
61− <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
62− <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))
63− <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))
64− <|> try (do cmd ["patt"]; t <- pFullExpr defaultSyntax; return (Pattelab t))
65− <|> do t <- pFullExpr defaultSyntax; return (Eval t)
66− <|> do eof; return NOP
26+pCmd = do spaces; try (do cmd ["q", "quit"]; eof; return Quit)
27+ <|> try (do cmd ["h", "?", "help"]; eof; return Help)
28+ <|> try (do cmd ["r", "reload"]; eof; return Reload)
29+ <|> try (do cmd ["m", "module"]; f <- identifier; eof;
30+ return (ModImport (toPath f)))
31+ <|> try (do cmd ["e", "edit"]; eof; return Edit)
32+ <|> try (do cmd ["exec", "execute"]; eof; return Execute)
33+ <|> try (do cmd ["ttshell"]; eof; return TTShell)
34+ <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
35+ <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
36+ <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))
37+ <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
38+ <|> try (do cmd ["proofs"]; eof; return Proofs)
39+ <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
40+ <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;
41+ return (Just x))
42+ eof; return (AddProof n))
43+ <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
44+ <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
45+ <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
46+ <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))
47+ <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))
48+ <|> try (do cmd ["spec"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Spec t))
49+ <|> try (do cmd ["hnf"]; whiteSpace; t <- pFullExpr defaultSyntax; return (HNF t))
50+ <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))
51+ <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))
52+ <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
53+ <|> try (do cmd ["t", "type"]; do whiteSpace; t <- pFullExpr defaultSyntax; return (Check t))
54+ <|> try (do cmd ["u", "universes"]; eof; return Universes)
55+ <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
56+ <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
57+ <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))
58+ <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
59+ <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))
60+ <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
61+ <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
62+ <|> try (do cmd ["s", "search"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Search t))
63+ <|> try (do cmd ["x"]; whiteSpace; t <- pFullExpr defaultSyntax; return (ExecVal t))
64+ <|> try (do cmd ["patt"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Pattelab t))
65+ <|> do whiteSpace; do eof; return NOP
66+ <|> do t <- pFullExpr defaultSyntax; return (Eval t)
6767
6868 where toPath n = foldl1' (</>) $ splitOn "." n
6969