@@ -23,205 +23,382 @@ import Data.List.Split(splitOn)
23import Data.Char(toLower)
23import Data.Char(toLower)
24import qualified Data.ByteString.UTF8 as UTF8
24import qualified Data.ByteString.UTF8 as UTF8
26−parseCmd :: IState -> String -> String -> Result Command
26+parseCmd :: IState -> String -> String -> Result (Either String Command)
27parseCmd i inputname = P.runparser pCmd i inputname
27parseCmd i inputname = P.runparser pCmd i inputname
29−cmd :: [String] -> P.IdrisParser ()
29+pCmd :: P.IdrisParser (Either String Command)
30−cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs))
31− where docmd [] = fail "No such command"
32− docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs
34−pCmd :: P.IdrisParser Command
36−pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit
30+pCmd = do c <- cmd ["q", "quit"]; noArgs c Quit
37− <|> do cmd ["h", "?", "help"]; eof; return Help
31+ <|> do c <- cmd ["h", "?", "help"]; noArgs c Help
38− <|> do cmd ["w", "warranty"]; eof; return Warranty
32+ <|> do c <- cmd ["w", "warranty"]; noArgs c Warranty
39− <|> do cmd ["r", "reload"]; eof; return Reload
33+ <|> do c <- cmd ["r", "reload"]; noArgs c 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
34+ <|> do c <- cmd ["exec", "execute"]; noArgs c Execute
44− <|> try (do cmd ["c", "compile"]
48− return (Compile (Via "c") f))
49− <|> do cmd ["c", "compile"]
55− <|> do cmd ["proofs"]; eof; return Proofs
35+ <|> do c <- cmd ["proofs"]; noArgs c Proofs
56− <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)
36+ <|> do c <- cmd ["u", "universes"]; noArgs c Universes
57− <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)
37+ <|> do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers
58− <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))
38+ <|> do c <- cmd ["m", "metavars"]; noArgs c Metavars
59− <|> do cmd ["let"]
39+ <|> do c <- cmd ["e", "edit"]; noArgs c Edit
60− defn <- concat <$> many (P.decl defaultSyntax)
40+
61− return (NewDefn defn)
41+ <|> do c <- cmd ["d", "def"]; fnNameArg c Defn
62− <|> do cmd ["unlet","undefine"]
63− Undefine `fmap` many P.name
64− <|> do cmd ["lto", "loadto"];
67− return (Load f (Just (fromInteger toline)))
68− <|> do cmd ["l", "load"]; f <- many anyChar;
69− return (Load f Nothing)
70− <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)
71− <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)
72− <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)
73− <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)
74− <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))
75− <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))
76− <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)
77− <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)
42+ <|> do c <- cmd ["total"]; fnNameArg c TotCheck
78− <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)
43+ <|> do c <- cmd ["printdef"]; fnNameArg c PrintDef
79− <|> do cmd ["u", "universes"]; eof; return Universes
44+ <|> do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls
45+ <|> do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho
80− <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)
46+ <|> do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo
81− <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)
47+ <|> do c <- cmd ["miss", "missing"]; fnNameArg c Missing
82− <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
48+
83− <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)
49+ <|> do c <- cmd ["t", "type"]; exprArg c Check
84− <|> do cmd ["color", "colour"]; pSetColourCmd
50+ <|> do c <- cmd ["x"]; exprArg c ExecVal
51+ <|> do c <- cmd ["patt"]; exprArg c Pattelab
52+ <|> do c <- cmd ["spec"]; exprArg c Spec
53+ <|> do c <- cmd ["hnf"]; exprArg c HNF
54+ <|> do c <- cmd ["inline"]; exprArg c TestInline
56+ <|> do c <- cmd ["rmproof"]; nameArg c RmProof
57+ <|> do c <- cmd ["showproof"]; nameArg c ShowProof
58+ <|> do c <- cmd ["p", "prove"]; nameArg c Prove
85− <|> do cmd ["set"]; o <- pOption; return (SetOpt o)
60+ <|> do c <- cmd ["set"]; optArg c SetOpt
86− <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)
61+ <|> do c <- cmd ["unset"]; optArg c UnsetOpt
87− <|> do cmd ["s", "search"]; P.whiteSpace;
62+
88− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)
63+ <|> do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)
64+ <|> do c <- cmd ["cd"]; strArg c ChangeDirectory
65+ <|> do c <- cmd ["apropos"]; strArg c Apropos
66+ <|> do c <- cmd ["mkdoc"]; strArg c MakeDoc
89− <|> do cmd ["cs", "casesplit"]; P.whiteSpace;
68+ <|> do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt
90− upd <- option False (do P.lchar '!'; return True)
91− l <- P.natural; n <- P.name;
92− return (CaseSplitAt upd (fromInteger l) n)
93− <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;
69+ <|> do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom
94− upd <- option False (do P.lchar '!'; return True)
95− l <- P.natural; n <- P.name;
96− return (AddProofClauseFrom upd (fromInteger l) n)
97− <|> do cmd ["ac", "addclause"]; P.whiteSpace;
70+ <|> do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom
98− upd <- option False (do P.lchar '!'; return True)
99− l <- P.natural; n <- P.name;
100− return (AddClauseFrom upd (fromInteger l) n)
101− <|> do cmd ["am", "addmissing"]; P.whiteSpace;
71+ <|> do c <- cmd ["am", "addmissing"]; proofArg c AddMissing
102− upd <- option False (do P.lchar '!'; return True)
103− l <- P.natural; n <- P.name;
104− return (AddMissing upd (fromInteger l) n)
105− <|> do cmd ["mw", "makewith"]; P.whiteSpace;
72+ <|> do c <- cmd ["mw", "makewith"]; proofArg c MakeWith
106− upd <- option False (do P.lchar '!'; return True)
107− l <- P.natural; n <- P.name;
108− return (MakeWith upd (fromInteger l) n)
109− <|> do cmd ["ml", "makelemma"]; P.whiteSpace;
73+ <|> do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma
110− upd <- option False (do P.lchar '!'; return True)
74+
111− l <- P.natural; n <- P.name;
75+ <|> do c <- cmd ["pp", "pprint"]; cmd_pprint c
112− return (MakeLemma upd (fromInteger l) n)
76+ <|> do c <- cmd ["doc"]; cmd_doc c
77+ <|> do c <- cmd ["dynamic"]; cmd_dynamic c
78+ <|> do c <- cmd ["consolewidth"]; cmd_consolewidth c
79+ <|> do c <- cmd ["module"]; cmd_module c
80+ <|> do c <- cmd ["c", "compile"]; cmd_compile c
81+ <|> do c <- cmd ["a", "addproof"]; cmd_addproof c
82+ <|> do c <- cmd ["log"]; cmd_log c
83+ <|> do c <- cmd ["let"]; cmd_let c
84+ <|> do c <- cmd ["unlet","undefine"]; cmd_unlet c
85+ <|> do c <- cmd ["lto", "loadto"]; cmd_loadto c
86+ <|> do c <- cmd ["color", "colour"]; cmd_colour c
87+ <|> do c <- cmd ["s", "search"]; cmd_search c
113− <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;
88+ <|> do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c
114− upd <- option False (do P.lchar '!'; return True)
115− l <- P.natural; n <- P.name;
116− hints <- many P.fnName
117− return (DoProofSearch upd True (fromInteger l) n hints)
118− <|> do cmd ["ref", "refine"]; P.whiteSpace;
89+ <|> do c <- cmd ["ref", "refine"]; cmd_refine c
119− upd <- option False (do P.lchar '!'; return True)
90+
120− l <- P.natural; n <- P.name;
91+ <|> unrecognized
121− hint <- P.fnName
92+ <|> nop
122− return (DoProofSearch upd False (fromInteger l) n [hint])
93+ <|> eval
123− <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)
94+
124− <|> do cmd ["m", "metavars"]; eof; return Metavars
95+ where nop = do P.whiteSpace; eof; return (Right NOP)
125− <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;
96+ eval = exprArg "" Eval
126− return (Just x))
97+ unrecognized = do
127− eof; return (AddProof n)
98+ P.lchar ':'
128− <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)
99+ cmd <- many anyChar
129− <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)
100+ let cmd' = takeWhile (/=' ') cmd
130− <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers
101+ return (Left $ "Unrecognized command: " ++ cmd')
131− <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)
102+
132− <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)
103+cmd :: [String] -> P.IdrisParser String
133− <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)
104+cmd xs = try $ do
134− <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)
105+ P.lchar ':'
135− <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)
106+ docmd sorted_xs
136− <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)
107+
137− <|> do cmd ["pp", "pprint"]
108+ where docmd [] = fail "Could not parse command"
138− P.whiteSpace
109+ docmd (x:xs) = try (P.reserved x >> return x) <|> docmd xs
140− P.whiteSpace
111+ sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs
141− n <- fmap fromInteger P.natural
112+
143− t <- P.fullExpr defaultSyntax
114+noArgs :: String -> Command -> P.IdrisParser (Either String Command)
144− return (PPrint fmt n t)
115+noArgs name cmd = do
145− <|> do P.whiteSpace; do eof; return NOP
116+ let emptyArgs = do
146− <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
117+ P.whiteSpace
148− where toPath n = foldl1' (</>) $ splitOn "." n
119+ return (Right cmd)
121+ let failure = return (Left $ ":" ++ name ++ " takes no arguments")
123+ try emptyArgs <|> failure
125+exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)
126+exprArg name cmd = do
130+ return $ Left ("Usage is :" ++ name ++ " <expression>")
133+ t <- P.fullExpr defaultSyntax
134+ return $ Right (cmd t)
135+ try noArg <|> properArg
138+fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
139+fnNameArg name cmd = do
141+ let emptyArgs = do eof
142+ return $ Left ("Usage is :" ++ name ++ " <functionname>")
143+ oneArg = do n <- P.fnName
145+ return (Right (cmd n))
146+ badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
147+ try emptyArgs <|> try oneArg <|> badArg
149+nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)
150+nameArg name cmd = do
152+ let emptyArgs = do eof
153+ return $ Left ("Usage is :" ++ name ++ " <functionname>")
154+ oneArg = do n <- P.name
156+ return (Right (cmd n))
157+ badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")
158+ try emptyArgs <|> try oneArg <|> badArg
160+strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)
164+ return (Right (cmd n))
166+optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)
170+ return $ Left ("Usage is :" ++ name ++ " <option>")
177+ return (Right (cmd o))
180+ return $ Left "Unrecognized setting"
182+ try emptyArgs <|> try oneArg <|> failure
150−pOption :: P.IdrisParser Opt
185+ pOption :: P.IdrisParser Opt
151−pOption = do discard (P.symbol "errorcontext"); return ErrContext
186+ pOption = do discard (P.symbol "errorcontext"); return ErrContext
152− <|> do discard (P.symbol "showimplicits"); return ShowImpl
187+ <|> do discard (P.symbol "showimplicits"); return ShowImpl
153− <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
188+ <|> do discard (P.symbol "originalerrors"); return ShowOrigErr
154− <|> do discard (P.symbol "autosolve"); return AutoSolve
189+ <|> do discard (P.symbol "autosolve"); return AutoSolve
155− <|> do discard (P.symbol "nobanner") ; return NoBanner
190+ <|> do discard (P.symbol "nobanner") ; return NoBanner
156− <|> do discard (P.symbol "warnreach"); return WarnReach
191+ <|> do discard (P.symbol "warnreach"); return WarnReach
158−codegenOption :: P.IdrisParser Codegen
193+proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)
159−codegenOption = do discard (P.symbol "bytecode"); return Bytecode
194+proofArg name cmd = do
160− <|> do x <- P.identifier
195+ P.whiteSpace
161− return (Via (map toLower x))
196+ upd <- option False $ do
201+ return (Right (cmd upd (fromInteger l) n))
203+cmd_doc :: String -> P.IdrisParser (Either String Command)
208+ return $ Right (DocStr (Right c))
213+ return $ Right (DocStr (Left falseTy))
215+ let fnName = fnNameArg name (\n -> DocStr (Left n))
217+ try constant <|> try bottom <|> fnName
219+cmd_consolewidth :: String -> P.IdrisParser (Either String Command)
220+cmd_consolewidth name = do
222+ return (Right (SetConsoleWidth w))
163−pConsoleWidth :: P.IdrisParser ConsoleWidth
225+ pConsoleWidth :: P.IdrisParser ConsoleWidth
164−pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
226+ pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth
165− <|> do discard (P.symbol "infinite"); return InfinitelyWide
227+ <|> do discard (P.symbol "infinite"); return InfinitelyWide
166− <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
228+ <|> do n <- fmap fromInteger P.natural; return (ColsWide n)
230+cmd_dynamic :: String -> P.IdrisParser (Either String Command)
231+cmd_dynamic name = do
232+ let emptyArgs = noArgs name ListDynamic
234+ let oneArg = do l <- many anyChar
235+ return $ Right (DynamicLink l)
237+ let failure = return $ Left $ "Usage is :" ++ name ++ " [<library>]"
239+ try emptyArgs <|> try oneArg <|> failure
241+cmd_pprint :: String -> P.IdrisParser (Either String Command)
246+ n <- fmap fromInteger P.natural
248+ t <- P.fullExpr defaultSyntax
249+ return (Right (PPrint fmt n t))
168−ppFormat :: P.IdrisParser OutputFmt
252+ ppFormat :: P.IdrisParser OutputFmt
169−ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
253+ ppFormat = (discard (P.symbol "html") >> return HTMLOutput)
170− <|> (discard (P.symbol "latex") >> return LaTeXOutput)
254+ <|> (discard (P.symbol "latex") >> return LaTeXOutput)
257+cmd_module :: String -> P.IdrisParser (Either String Command)
261+ return (Right (ModImport (toPath f)))
263+ toPath n = foldl1' (</>) $ splitOn "." n
265+cmd_compile :: String -> P.IdrisParser (Either String Command)
266+cmd_compile name = do
267+ let defaultCodegen = Via "c"
269+ let codegenOption :: P.IdrisParser Codegen
271+ let bytecodeCodegen = discard (P.symbol "bytecode") *> return Bytecode
272+ viaCodegen = do x <- P.identifier
273+ return (Via (map toLower x))
274+ bytecodeCodegen <|> viaCodegen
280+ return $ Right (Compile defaultCodegen f)
284+ codegen <- codegenOption
287+ return $ Right (Compile codegen f)
289+ let failure = return $ Left $ "Usage is :" ++ name ++ " [<codegen>] <filename>"
290+ try hasTwoArgs <|> try hasOneArg <|> failure
292+cmd_addproof :: String -> P.IdrisParser (Either String Command)
293+cmd_addproof name = do
294+ n <- option Nothing $ do
298+ return (Right (AddProof n))
300+cmd_log :: String -> P.IdrisParser (Either String Command)
304+ return (Right (LogLvl (fromIntegral i)))
306+cmd_let :: String -> P.IdrisParser (Either String Command)
308+ defn <- concat <$> many (P.decl defaultSyntax)
309+ return (Right (NewDefn defn))
311+cmd_unlet :: String -> P.IdrisParser (Either String Command)
313+ (Right . Undefine) `fmap` many P.name
315+cmd_loadto :: String -> P.IdrisParser (Either String Command)
319+ return (Right (Load f (Just (fromInteger toline))))
321+cmd_colour :: String -> P.IdrisParser (Either String Command)
323+ pSetColourCmd >>= return . Right
172−colours :: [(String, Maybe Color)]
326+ colours :: [(String, Maybe Color)]
173−colours = [ ("black", Just Black)
327+ colours = [ ("black", Just Black)
174− , ("red", Just Red)
328+ , ("red", Just Red)
175− , ("green", Just Green)
329+ , ("green", Just Green)
176− , ("yellow", Just Yellow)
330+ , ("yellow", Just Yellow)
177− , ("blue", Just Blue)
331+ , ("blue", Just Blue)
178− , ("magenta", Just Magenta)
332+ , ("magenta", Just Magenta)
179− , ("cyan", Just Cyan)
333+ , ("cyan", Just Cyan)
180− , ("white", Just White)
334+ , ("white", Just White)
181− , ("default", Nothing)
335+ , ("default", Nothing)
338+ pSetColourCmd :: P.IdrisParser Command
339+ pSetColourCmd = (do c <- pColourType
340+ let defaultColour = IdrisColour Nothing True False False False
341+ opts <- sepBy pColourMod (P.whiteSpace)
342+ let colour = foldr ($) defaultColour $ reverse opts
343+ return $ SetColour c colour)
344+ <|> try (P.symbol "on" >> return ColourOn)
345+ <|> try (P.symbol "off" >> return ColourOff)
184−pColour :: P.IdrisParser (Maybe Color)
347+ pColour :: P.IdrisParser (Maybe Color)
185−pColour = doColour colours
348+ pColour = doColour colours
186− where doColour [] = fail "Unknown colour"
349+ where doColour [] = fail "Unknown colour"
187− doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
350+ doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs
189−pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
352+ pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)
190−pColourMod = try (P.symbol "vivid" >> return doVivid)
353+ pColourMod = try (P.symbol "vivid" >> return doVivid)
191− <|> try (P.symbol "dull" >> return doDull)
354+ <|> try (P.symbol "dull" >> return doDull)
192− <|> try (P.symbol "underline" >> return doUnderline)
355+ <|> try (P.symbol "underline" >> return doUnderline)
193− <|> try (P.symbol "nounderline" >> return doNoUnderline)
356+ <|> try (P.symbol "nounderline" >> return doNoUnderline)
194− <|> try (P.symbol "bold" >> return doBold)
357+ <|> try (P.symbol "bold" >> return doBold)
195− <|> try (P.symbol "nobold" >> return doNoBold)
358+ <|> try (P.symbol "nobold" >> return doNoBold)
196− <|> try (P.symbol "italic" >> return doItalic)
359+ <|> try (P.symbol "italic" >> return doItalic)
197− <|> try (P.symbol "noitalic" >> return doNoItalic)
360+ <|> try (P.symbol "noitalic" >> return doNoItalic)
198− <|> try (pColour >>= return . doSetColour)
361+ <|> try (pColour >>= return . doSetColour)
199− where doVivid i = i { vivid = True }
362+ where doVivid i = i { vivid = True }
200− doDull i = i { vivid = False }
363+ doDull i = i { vivid = False }
201− doUnderline i = i { underline = True }
364+ doUnderline i = i { underline = True }
202− doNoUnderline i = i { underline = False }
365+ doNoUnderline i = i { underline = False }
203− doBold i = i { bold = True }
366+ doBold i = i { bold = True }
204− doNoBold i = i { bold = False }
367+ doNoBold i = i { bold = False }
205− doItalic i = i { italic = True }
368+ doItalic i = i { italic = True }
206− doNoItalic i = i { italic = False }
369+ doNoItalic i = i { italic = False }
207− doSetColour c i = i { colour = c }
370+ doSetColour c i = i { colour = c }
209−-- | Generate the colour type names using the default Show instance.
372+ -- | Generate the colour type names using the default Show instance.
210−colourTypes :: [(String, ColourType)]
373+ colourTypes :: [(String, ColourType)]
211−colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
374+ colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $
212− enumFromTo minBound maxBound
375+ enumFromTo minBound maxBound
214−pColourType :: P.IdrisParser ColourType
377+ pColourType :: P.IdrisParser ColourType
215−pColourType = doColourType colourTypes
378+ pColourType = doColourType colourTypes
216− where doColourType [] = fail $ "Unknown colour category. Options: " ++
379+ where doColourType [] = fail $ "Unknown colour category. Options: " ++
217− (concat . intersperse ", " . map fst) colourTypes
380+ (concat . intersperse ", " . map fst) colourTypes
218− doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
381+ doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts
220−pSetColourCmd :: P.IdrisParser Command
384+cmd_search :: String -> P.IdrisParser (Either String Command)
221−pSetColourCmd = (do c <- pColourType
385+cmd_search name = do
222− let defaultColour = IdrisColour Nothing True False False False
386+ P.whiteSpace;
387+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True })
388+ return (Right (Search t))
390+cmd_proofsearch :: String -> P.IdrisParser (Either String Command)
391+cmd_proofsearch name = do
223− opts <- sepBy pColourMod (P.whiteSpace)
392+ P.whiteSpace
224− let colour = foldr ($) defaultColour $ reverse opts
393+ upd <- option False (do P.lchar '!'; return True)
225− return $ SetColour c colour)
394+ l <- P.natural; n <- P.name;
226− <|> try (P.symbol "on" >> return ColourOn)
395+ hints <- many P.fnName
227− <|> try (P.symbol "off" >> return ColourOff)
396+ return (Right (DoProofSearch upd True (fromInteger l) n hints))
398+cmd_refine :: String -> P.IdrisParser (Either String Command)
401+ upd <- option False (do P.lchar '!'; return True)
402+ l <- P.natural; n <- P.name;
404+ return (Right (DoProofSearch upd False (fromInteger l) n [hint]))