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