@@ -199,56 +199,57 @@ ideslave orig mods
199199 Right (sexp, id) -> return (sexp, id)
200200 i <- getIState
201201 putIState $ i { idris_outputmode = (IdeSlave id) }
202− let fn = case mods of
203− (f:_) -> f
204− _ -> ""
205− case IdeSlave.sexpToCommand sexp of
206− Just (IdeSlave.Interpret cmd) ->
207− do c <- colourise
208− case parseCmd i "(input)" cmd of
209− Failure err -> iPrintError $ show (fixColour c err)
210− Success (Prove n') -> do iPrintResult ""
211− idrisCatch
212− (process stdout fn (Prove n'))
213− (\e -> getIState >>= iPrintError . flip pshow e)
214− isetPrompt (mkPrompt mods)
215− Success cmd -> idrisCatch
216− (ideslaveProcess fn cmd)
217− (\e -> getIState >>= iPrintError . flip pshow e)
218− Just (IdeSlave.REPLCompletions str) ->
219− do (unused, compls) <- replCompletion (reverse str, "")
220− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
221− runIO $ putStrLn $ IdeSlave.convSExp "return" good id
222− Just (IdeSlave.LoadFile filename) ->
223− do clearErr
224− putIState (orig { idris_options = idris_options i,
225− idris_outputmode = (IdeSlave id) })
226− idrisCatch (do mod <- loadModule' stdout filename
227− return ())
228− (setAndReport)
229− isetPrompt (mkPrompt [filename])
230−
231− -- Report either success or failure
232− i <- getIState
233− case (errLine i) of
234− Nothing -> iPrintResult $ "loaded " ++ filename
235− Just x -> iPrintError $ "didn't load " ++ filename
236− ideslave orig [filename]
237− Just (IdeSlave.TypeOf name) ->
238− process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))
239− Just (IdeSlave.CaseSplit line name) ->
240− process stdout fn (CaseSplitAt False line (UN name))
241− Just (IdeSlave.AddClause line name) ->
242− process stdout fn (AddClauseFrom False line (UN name))
243− Just (IdeSlave.AddProofClause line name) ->
244− process stdout fn (AddProofClauseFrom False line (UN name))
245− Just (IdeSlave.AddMissing line name) ->
246− process stdout fn (AddMissing False line (UN name))
247− Just (IdeSlave.MakeWithBlock line name) ->
248− process stdout fn (MakeWith False line (UN name))
249− Just (IdeSlave.ProofSearch line name hints) ->
250− process stdout fn (DoProofSearch False line (UN name) (map UN hints))
251− Nothing -> do iPrintError "did not understand")
202+ idrisCatch -- to report correct id back!
203+ (do let fn = case mods of
204+ (f:_) -> f
205+ _ -> ""
206+ case IdeSlave.sexpToCommand sexp of
207+ Just (IdeSlave.Interpret cmd) ->
208+ do c <- colourise
209+ case parseCmd i "(input)" cmd of
210+ Failure err -> iPrintError $ show (fixColour c err)
211+ Success (Prove n') -> do iPrintResult ""
212+ idrisCatch
213+ (process stdout fn (Prove n'))
214+ (\e -> getIState >>= iPrintError . flip pshow e)
215+ isetPrompt (mkPrompt mods)
216+ Success cmd -> idrisCatch
217+ (ideslaveProcess fn cmd)
218+ (\e -> getIState >>= iPrintError . flip pshow e)
219+ Just (IdeSlave.REPLCompletions str) ->
220+ do (unused, compls) <- replCompletion (reverse str, "")
221+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
222+ runIO $ putStrLn $ IdeSlave.convSExp "return" good id
223+ Just (IdeSlave.LoadFile filename) ->
224+ do clearErr
225+ putIState (orig { idris_options = idris_options i,
226+ idris_outputmode = (IdeSlave id) })
227+ idrisCatch (do mod <- loadModule' stdout filename
228+ return ())
229+ (setAndReport)
230+ isetPrompt (mkPrompt [filename])
231+ -- Report either success or failure
232+ i <- getIState
233+ case (errLine i) of
234+ Nothing -> iPrintResult $ "loaded " ++ filename
235+ Just x -> iPrintError $ "didn't load " ++ filename
236+ ideslave orig [filename]
237+ Just (IdeSlave.TypeOf name) ->
238+ process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))
239+ Just (IdeSlave.CaseSplit line name) ->
240+ process stdout fn (CaseSplitAt False line (UN name))
241+ Just (IdeSlave.AddClause line name) ->
242+ process stdout fn (AddClauseFrom False line (UN name))
243+ Just (IdeSlave.AddProofClause line name) ->
244+ process stdout fn (AddProofClauseFrom False line (UN name))
245+ Just (IdeSlave.AddMissing line name) ->
246+ process stdout fn (AddMissing False line (UN name))
247+ Just (IdeSlave.MakeWithBlock line name) ->
248+ process stdout fn (MakeWith False line (UN name))
249+ Just (IdeSlave.ProofSearch line name hints) ->
250+ process stdout fn (DoProofSearch False line (UN name) (map UN hints))
251+ Nothing -> do iPrintError "did not understand")
252+ (\e -> do iPrintError $ show e))
252253 (\e -> do iPrintError $ show e)
253254 ideslave orig mods
254255