@@ -19,13 +19,13 @@ import Idris.Parser hiding (params)
19import Idris.Error
19import Idris.Error
20import Idris.DataOpts
20import Idris.DataOpts
21import Idris.Completion
21import Idris.Completion
22−import Idris.IdeSlave
22+import qualified Idris.IdeSlave as IdeSlave
23import Idris.Output
23import Idris.Output
24import Idris.TypeSearch (searchByType)
24import Idris.TypeSearch (searchByType)
26import Text.Trifecta.Result(Result(..))
26import Text.Trifecta.Result(Result(..))
28−import System.IO (Handle)
28+import System.IO (Handle , stdin, stdout)
29import System.Console.Haskeline
29import System.Console.Haskeline
30import System.Console.Haskeline.History
30import System.Console.Haskeline.History
31import Control.Monad.State.Strict
31import Control.Monad.State.Strict
@@ -95,7 +95,7 @@ prove opt ctxt lit n ty
95 solveDeferred n
95 solveDeferred n
96 case idris_outputmode i of
96 case idris_outputmode i of
97 IdeSlave n _ ->
97 IdeSlave n _ ->
98− iputStrLn $ convSExp "return" (SymbolAtom "ok", "") n
98+ iputStrLn $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n
99 _ -> return ()
99 _ -> return ()
101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])
@@ -180,20 +180,25 @@ lifte st e = do (v, _) <- elabStep st e
180receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)
180receiveInput :: Handle -> ElabState [PDecl] -> Idris (Maybe String)
181receiveInput h e =
181receiveInput h e =
182 do i <- getIState
182 do i <- getIState
183− l <- runIO $ getLine
183+ let inh = if h == stdout then stdin else h
184+ len' <- runIO $ IdeSlave.getLen inh
186+ Left err -> ierror err
188+ l <- runIO $ IdeSlave.getNChar inh len ""
184− (sexp, id) <- case parseMessage l of
189+ (sexp, id) <- case IdeSlave.parseMessage l of
185 Left err -> ierror err
190 Left err -> ierror err
186 Right (sexp, id) -> return (sexp, id)
191 Right (sexp, id) -> return (sexp, id)
187 putIState $ i { idris_outputmode = (IdeSlave id h) }
192 putIState $ i { idris_outputmode = (IdeSlave id h) }
188− case sexpToCommand sexp of
193+ case IdeSlave.sexpToCommand sexp of
189− Just (REPLCompletions prefix) ->
194+ Just (IdeSlave.REPLCompletions prefix) ->
190 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")
195 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)]
192 ideslavePutSExp "return" good
197 ideslavePutSExp "return" good
193 receiveInput h e
198 receiveInput h e
194− Just (Interpret cmd) -> return (Just cmd)
199+ Just (IdeSlave.Interpret cmd) -> return (Just cmd)
195− Just (TypeOf str) -> return (Just (":t " ++ str))
200+ Just (IdeSlave.TypeOf str) -> return (Just (":t " ++ str))
196− Just (DocsFor str) -> return (Just (":doc " ++ str))
201+ Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))
197 _ -> return Nothing
202 _ -> return Nothing
199ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
204ploop :: Name -> Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])