@@ -17,7 +17,7 @@ import Idris.UnusedArgs
1717import Idris.Docs
1818import Idris.Help
1919import Idris.Completion
20−import Idris.IdeSlave
20+import qualified Idris.IdeSlave as IdeSlave
2121import Idris.Chaser
2222import Idris.Imports
2323import Idris.Colours
@@ -194,17 +194,17 @@ ideslave :: IState -> [FilePath] -> Idris ()
194194ideslave orig mods
195195 = do idrisCatch
196196 (do l <- runIO $ getLine
197− (sexp, id) <- case parseMessage l of
197+ (sexp, id) <- case IdeSlave.parseMessage l of
198198 Left err -> ierror err
199199 Right (sexp, id) -> return (sexp, id)
200200 i <- getIState
201201 putIState $ i { idris_outputmode = (IdeSlave id) }
202− case sexpToCommand sexp of
203− Just (Interpret cmd) ->
204− do let fn = case mods of
205− (f:_) -> f
206− _ -> ""
207− c <- colourise
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
208208 case parseCmd i "(input)" cmd of
209209 Failure err -> iPrintError $ show (fixColour c err)
210210 Success (Prove n') -> do iPrintResult ""
@@ -215,11 +215,11 @@ ideslave orig mods
215215 Success cmd -> idrisCatch
216216 (ideslaveProcess fn cmd)
217217 (\e -> getIState >>= iPrintError . flip pshow e)
218− Just (REPLCompletions str) ->
218+ Just (IdeSlave.REPLCompletions str) ->
219219 do (unused, compls) <- replCompletion (reverse str, "")
220− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
221− runIO $ putStrLn $ convSExp "return" good id
222− Just (LoadFile filename) ->
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) ->
223223 do clearErr
224224 putIState (orig { idris_options = idris_options i,
225225 idris_outputmode = (IdeSlave id) })
@@ -233,8 +233,10 @@ ideslave orig mods
233233 Nothing -> iPrintResult $ "loaded " ++ filename
234234 Just x -> iPrintError $ "didn't load " ++ filename
235235 ideslave orig [filename]
236− Just (TypeOf name) ->
236+ Just (IdeSlave.TypeOf name) ->
237237 process stdout "(ideslave)" (Check (PRef (FC "(ideslave)" 0 0) (UN name)))
238+ Just (IdeSlave.CaseSplit line name) ->
239+ process stdout fn (CaseSplitAt False line (UN name))
238240 Nothing -> do iPrintError "did not understand")
239241 (\e -> do iPrintError $ show e)
240242 ideslave orig mods
@@ -550,12 +552,12 @@ process h fn (CaseSplitAt updatefile l n)
550552 let (before, (ap : later)) = splitAt (l-1) (lines src)
551553 res' <- replaceSplits ap res
552554 let new = concat res'
553− if updatefile then
554− do let fb = fn ++ "~" -- make a backup!
555− runIO $ writeFile fb (unlines before ++ new ++ unlines later)
556− runIO $ copyFile fb fn
557− else -- do ihputStrLn h (show res)
558− ihputStrLn h new
555+ if updatefile
556+ then do let fb = fn ++ "~" -- make a backup!
557+ runIO $ writeFile fb (unlines before ++ new ++ unlines later)
558+ runIO $ copyFile fb fn
559+ else -- do ihputStrLn h (show res)
560+ ihPrintResult h new
559561process h fn (AddClauseFrom updatefile l n)
560562 = do src <- runIO $ readFile fn
561563 let (before, tyline : later) = splitAt (l-1) (lines src)