@@ -19,13 +19,13 @@ import Idris.Parser hiding (params)
1919import Idris.Error
2020import Idris.DataOpts
2121import Idris.Completion
22−import Idris.IdeSlave
22+import qualified Idris.IdeSlave as IdeSlave
2323import Idris.Output
2424import Idris.TypeSearch (searchByType)
2525
2626import Text.Trifecta.Result(Result(..))
2727
28−import System.IO (Handle)
28+import System.IO (Handle , stdin, stdout)
2929import System.Console.Haskeline
3030import System.Console.Haskeline.History
3131import Control.Monad.State.Strict
@@ -95,7 +95,7 @@ prove opt ctxt lit n ty
9595 solveDeferred n
9696 case idris_outputmode i of
9797 IdeSlave n _ ->
98− iputStrLn $ convSExp "return" (SymbolAtom "ok", "") n
98+ iputStrLn $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n
9999 _ -> return ()
100100
101101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
@@ -180,20 +180,25 @@ lifte st e = do (v, _) <- elabStep st e
180180receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)
181181receiveInput h e =
182182 do i <- getIState
183− l <- runIO $ getLine
184− (sexp, id) <- case parseMessage l of
183+ let inh = if h == stdout then stdin else h
184+ len' <- runIO $ IdeSlave.getLen inh
185+ len <- case len' of
186+ Left err -> ierror err
187+ Right n -> return n
188+ l <- runIO $ IdeSlave.getNChar inh len ""
189+ (sexp, id) <- case IdeSlave.parseMessage l of
185190 Left err -> ierror err
186191 Right (sexp, id) -> return (sexp, id)
187192 putIState $ i { idris_outputmode = (IdeSlave id h) }
188− case sexpToCommand sexp of
189− Just (REPLCompletions prefix) ->
193+ case IdeSlave.sexpToCommand sexp of
194+ Just (IdeSlave.REPLCompletions prefix) ->
190195 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
191− let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]
196+ let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]
192197 ideslavePutSExp "return" good
193198 receiveInput h e
194− Just (Interpret cmd) -> return (Just cmd)
195− Just (TypeOf str) -> return (Just (":t " ++ str))
196− Just (DocsFor str) -> return (Just (":doc " ++ str))
199+ Just (IdeSlave.Interpret cmd) -> return (Just cmd)
200+ Just (IdeSlave.TypeOf str) -> return (Just (":t " ++ str))
201+ Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))
197202 _ -> return Nothing
198203
199204ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])