1add7b7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

provide a Handle for IdeSlave, used to read from and write to (instead of hardcoded stdin/stdout)

also send protocol-version message when the client connects also accept a single client connection when --ideslave-socket is provided (I don't see any reason to have multiple clients at all!)

commit1add7b7a7d8b74cf72a7247115eb3a864f7c3ce8 authorHannes Mehnert <hannes@mehnert.org> dateSat 2 Aug 2014, 21:00 (12 years ago) parentbe0a480

9 files changed+144−121

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+9−9 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/IdeSlave.hs+7−10 src/Idris/Interactive.hs+4−4 src/Idris/Output.hs+16−16 src/Idris/Parser.hs+2−2 src/Idris/Prover.hs+11−11 src/Idris/REPL.hs+91−65 src/Idris/TypeSearch.hs+3−3

src/Idris/AbsSyntax.hs+9−9

@@ -537,7 +537,7 @@ type1Doc = (annotate (AnnType "Type" "The type of types, one level up") $ text "

537537isetPrompt :: String -> Idris ()

538538isetPrompt p = do i <- getIState

539539 case idris_outputmode i of

540− IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

540+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

541541

542542-- | Tell clients how much was parsed and loaded

543543isetLoadedRegion :: Idris ()

@@ -546,8 +546,8 @@ isetLoadedRegion = do i <- getIState

546546 case span of

547547 Just fc ->

548548 case idris_outputmode i of

549− IdeSlave n ->

550− runIO . putStrLn $

549+ IdeSlave n h ->

550+ runIO . hPutStrLn h $

551551 convSExp "set-loaded-region" fc n

552552 Nothing -> return ()

553553

@@ -662,10 +662,10 @@ outputTy :: Idris OutputType

662662outputTy = do i <- getIState

663663 return $ opt_outputTy $ idris_options i

664664

665−setIdeSlave :: Bool -> Idris ()

666−setIdeSlave True = do i <- getIState

667− putIState $ i { idris_outputmode = (IdeSlave 0), idris_colourRepl = False }

668−setIdeSlave False = return ()

665+setIdeSlave :: Bool -> Handle -> Idris ()

666+setIdeSlave True h = do i <- getIState

667+ putIState $ i { idris_outputmode = (IdeSlave 0 h), idris_colourRepl = False }

668+setIdeSlave False _ = return ()

669669

670670setTargetTriple :: String -> Idris ()

671671setTargetTriple t = do i <- getIState

@@ -794,9 +794,9 @@ logLvl l str = do i <- getIState

794794 when (lvl >= l) $

795795 case idris_outputmode i of

796796 RawOutput -> do runIO $ putStrLn str

797− IdeSlave n ->

797+ IdeSlave n h ->

798798 do let good = SexpList [IntegerAtom (toInteger l), toSExp str]

799− runIO $ putStrLn $ convSExp "log" good n

799+ runIO . hPutStrLn h $ convSExp "log" good n

800800

801801cmdOptType :: Opt -> Idris Bool

802802cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1−1

@@ -127,7 +127,7 @@ ppOptionIst = ppOption . idris_options

127127data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

128128

129129-- | The output mode in use

130−data OutputMode = RawOutput | IdeSlave Integer deriving Show

130+data OutputMode = RawOutput | IdeSlave Integer Handle deriving Show

131131

132132-- | How wide is the console?

133133data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken

src/Idris/IdeSlave.hs+7−10

@@ -1,6 +1,6 @@

11{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

3−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..)) where

3+module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch) where

55import Text.Printf

66import Numeric

@@ -251,15 +251,9 @@ parseMessage x = case receiveString x of

251251

252252receiveString :: String -> Either Err SExp

253253receiveString x =

254− case readHex (take 6 x) of

255− ((num, ""):_) ->

256− let msg = drop 6 x in

257− if (length msg) /= (num - 1)

258− then Left . Msg $ "bad input length"

259− else (case parseSExp msg of

260− Failure _ -> Left . Msg $ "parse failure"

261− Success r -> Right r)

262− _ -> Left . Msg $ "readHex failed"

254+ case parseSExp x of

255+ Failure _ -> Left . Msg $ "parse failure"

256+ Success r -> Right r

263257

264258convSExp :: SExpable a => String -> a -> Integer -> String

265259convSExp pre s id =

@@ -269,3 +263,6 @@ convSExp pre s id =

269263

270264getHexLength :: String -> String

271265getHexLength s = printf "%06x" (1 + (length s))

266+

267+ideSlaveEpoch :: Int

268+ideSlaveEpoch = 1

src/Idris/Interactive.hs+4−4

@@ -266,8 +266,8 @@ makeLemma h fn updatefile l n

266266 runIO $ writeFile fb (addLem before tyline lem lem_app later)

267267 runIO $ copyFile fb fn

268268 else case idris_outputmode i of

269− RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

270− IdeSlave n ->

269+ RawOutput -> ihPrintResult h $ lem ++ "\n" ++ lem_app

270+ IdeSlave n h ->

271271 let good = SexpList [SymbolAtom "ok",

272272 SexpList [SymbolAtom "metavariable-lemma",

273273 SexpList [SymbolAtom "replace-metavariable",

@@ -284,8 +284,8 @@ makeLemma h fn updatefile l n

284284 runIO $ writeFile fb (addProv before tyline lem_app later)

285285 runIO $ copyFile fb fn

286286 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

288− IdeSlave n ->

287+ RawOutput -> ihPrintResult h $ lem_app

288+ IdeSlave n h ->

289289 let good = SexpList [SymbolAtom "ok",

290290 SexpList [SymbolAtom "provisional-definition-lemma",

291291 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+16−16

@@ -33,7 +33,7 @@ ihWarn h fc err = do i <- getIState

3333 then text (show fc) <> colon <//> err

3434 else err

3535 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

36− IdeSlave n ->

36+ IdeSlave n h ->

3737 do err' <- iRender . fmap (fancifyAnnots i) $ err

3838 let (str, spans) = displaySpans err'

3939 runIO . hPutStrLn h $

@@ -43,8 +43,8 @@ iRender :: Doc a -> Idris (SimpleDoc a)

4343iRender d = do w <- getWidth

4444 ist <- getIState

4545 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

47− _ -> False

46+ IdeSlave _ _ -> True

47+ _ -> False

4848 case w of

4949 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

5050 ColsWide n -> return $

@@ -84,16 +84,16 @@ ihRenderOutput h doc =

8484 case idris_outputmode i of

8585 RawOutput -> do out <- iRender doc

8686 runIO $ putStrLn (displayDecorated (consoleDecorate i) out)

87− IdeSlave n ->

87+ IdeSlave n h ->

8888 do (str, spans) <- fmap displaySpans . iRender . fmap (fancifyAnnots i) $ doc

8989 let out = [toSExp str, toSExp spans]

90− runIO . putStrLn $ convSExp "write-decorated" out n

90+ runIO . hPutStrLn h $ convSExp "write-decorated" out n

9191

9292ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

9393ihRenderResult h d = do ist <- getIState

9494 case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

95+ RawOutput -> consoleDisplayAnnotated h d

96+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

9797

9898ideSlaveReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

9999ideSlaveReturnWithStatus status n h out = do

@@ -114,17 +114,17 @@ ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

114114ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

115115ihRenderError h e = do ist <- getIState

116116 case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

118− IdeSlave n -> ideSlaveReturnWithStatus "error" n h e

117+ RawOutput -> consoleDisplayAnnotated h e

118+ IdeSlave n h -> ideSlaveReturnWithStatus "error" n h e

119119

120120ihPrintWithStatus :: String -> Handle -> String -> Idris ()

121−ihPrintWithStatus status h s = do

121+ihPrintWithStatus status h s = do

122122 i <- getIState

123123 case idris_outputmode i of

124124 RawOutput -> case s of

125125 "" -> return ()

126126 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

127+ IdeSlave n h ->

128128 let good = SexpList [SymbolAtom status, toSExp s] in

129129 runIO $ hPutStrLn h $ convSExp "return" good n

130130

@@ -138,8 +138,8 @@ ihPrintError = ihPrintWithStatus "error"

138138ihputStrLn :: Handle -> String -> Idris ()

139139ihputStrLn h s = do i <- getIState

140140 case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

142− IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

141+ RawOutput -> runIO $ hPutStrLn h s

142+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

143143

144144iputStrLn = ihputStrLn stdout

145145iPrintError = ihPrintError stdout

@@ -149,7 +149,7 @@ iWarn = ihWarn stdout

149149ideslavePutSExp :: SExpable a => String -> a -> Idris ()

150150ideslavePutSExp cmd info = do i <- getIState

151151 case idris_outputmode i of

152− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

152+ IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n

153153 _ -> return ()

154154

155155-- TODO: send structured output similar to the metavariable list

@@ -157,10 +157,10 @@ iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

157157iputGoal g = do i <- getIState

158158 case idris_outputmode i of

159159 RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

160− IdeSlave n ->

160+ IdeSlave n h ->

161161 let (str, spans) = displaySpans . fmap (fancifyAnnots i) $ g

162162 goal = [toSExp str, toSExp spans]

163− in runIO . putStrLn $ convSExp "write-goal" goal n

163+ in runIO . hPutStrLn h $ convSExp "write-goal" goal n

164164

165165-- | Warn about totality problems without failing to compile

166166warnTotality :: Idris ()

src/Idris/Parser.hs+2−2

@@ -1159,8 +1159,8 @@ parseProg syn fname input mrk

11591159 let (fc, msg) = findFC doc

11601160 i <- getIState

11611161 case idris_outputmode i of

1162− RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1163− IdeSlave n -> ihWarn (idris_outh i) fc (P.text msg)

1162+ RawOutput -> ihputStrLn (idris_outh i) (show $ fixColour (idris_colourRepl i) doc)

1163+ IdeSlave n h -> ihWarn h fc (P.text msg)

11641164 putIState (i { errSpan = Just fc })

11651165 return []

11661166 Success (x, i) -> do putIState i

src/Idris/Prover.hs+11−11

@@ -27,6 +27,7 @@ import Text.Trifecta.Result(Result(..))

2727

2828import System.Console.Haskeline

2929import System.Console.Haskeline.History

30+import System.IO (Handle)

3031import Control.Monad.State.Strict

3132import Control.DeepSeq

3233

@@ -70,8 +71,8 @@ prove opt ctxt lit n ty

7071 iLOG $ "Adding " ++ show tm

7172 i <- getIState

7273 case idris_outputmode i of

73− IdeSlave _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

74− _ -> iputStrLn $ showProof lit n prf

74+ IdeSlave _ _ -> ideslavePutSExp "end-proof-mode" (n, showProof lit n prf)

75+ _ -> iputStrLn $ showProof lit n prf

7576 let proofs = proof_list i

7677 putIState (i { proof_list = (n, prf) : proofs })

7778 let tree = simpleCase False True False CompileTime (fileFC "proof") [] [] [([], P Ref n ty, tm)]

@@ -93,9 +94,8 @@ prove opt ctxt lit n ty

9394 [([], P Ref n ty, ptm')] ty)

9495 solveDeferred n

9596 case idris_outputmode i of

96− IdeSlave n ->

97− runIO . putStrLn $

98− convSExp "return" (SymbolAtom "ok", "") n

97+ IdeSlave n h ->

98+ ihputStrLn h $ convSExp "return" (SymbolAtom "ok", "") n

9999 _ -> return ()

100100

101101elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

@@ -177,20 +177,20 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a

177177lifte st e = do (v, _) <- elabStep st e

178178 return v

179179

180−receiveInput :: ElabState [PDecl] -> Idris (Maybe String)

181−receiveInput e =

180+receiveInput :: ElabState [PDecl] -> Handle -> Idris (Maybe String)

181+receiveInput e handle =

182182 do i <- getIState

183183 l <- runIO $ getLine

184184 (sexp, id) <- case parseMessage l of

185185 Left err -> ierror err

186186 Right (sexp, id) -> return (sexp, id)

187− putIState $ i { idris_outputmode = (IdeSlave id) }

187+ putIState $ i { idris_outputmode = (IdeSlave id handle) }

188188 case sexpToCommand sexp of

189189 Just (REPLCompletions prefix) ->

190190 do (unused, compls) <- proverCompletion (assumptionNames e) (reverse prefix, "")

191191 let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]

192192 ideslavePutSExp "return" good

193− receiveInput e

193+ receiveInput e handle

194194 Just (Interpret cmd) -> return (Just cmd)

195195 Just (TypeOf str) -> return (Just (":t " ++ str))

196196 Just (DocsFor str) -> return (Just (":doc " ++ str))

@@ -211,9 +211,9 @@ ploop fn d prompt prf e h

211211 l <- getInputLine (prompt ++ "> ")

212212 h' <- getHistory

213213 return (l, Just h')

214− IdeSlave n ->

214+ IdeSlave _ handle ->

215215 do isetPrompt prompt

216− i <- receiveInput e

216+ i <- receiveInput e handle

217217 return (i, h)

218218 (cmd, step) <- case x of

219219 Nothing -> do iPrintError ""; ifail "Abandoned"

src/Idris/REPL.hs+91−65

@@ -42,7 +42,7 @@ import Idris.Elab.Value

4242import Version_idris (gitHash)

4343import Util.System

4444import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

4646import Util.Pretty hiding ((</>))

4747

4848import Idris.Core.Evaluate

@@ -91,6 +91,8 @@ import Data.Word (Word)

9191import Data.Either (partitionEithers)

9292import Control.DeepSeq

9393

94+import Numeric ( readHex )

95+

9496import Debug.Trace

9597

9698-- | Run the REPL

@@ -206,44 +208,68 @@ runClient str = withSocketsDo $ do

206208 else do l <- hGetLine h

207209 hGetResp (acc ++ l ++ "\n") h

208210

211+initIdeslaveSocket :: IO (Handle)

212+initIdeslaveSocket = do

213+ (sock, port) <- listenOnLocalhostAnyPort

214+ putStrLn $ show port

215+ (h, _, _) <- accept sock

216+ hSetEncoding h utf8

217+ return h

218+

209219-- | Run the IdeSlave

210−ideslaveStart :: IState -> [FilePath] -> Idris ()

211−ideslaveStart orig mods

212− = do i <- getIState

220+ideslaveStart :: Bool -> IState -> [FilePath] -> Idris ()

221+ideslaveStart s orig mods

222+ = do h <- runIO $ if s then initIdeslaveSocket else return stdout

223+ setIdeSlave True h

224+ i <- getIState

213225 case idris_outputmode i of

214− IdeSlave n ->

215− when (mods /= []) (do isetPrompt (mkPrompt mods))

216− ideslave orig mods

217−

218−

219−ideslave :: IState -> [FilePath] -> Idris ()

220−ideslave orig mods

226+ IdeSlave n h ->

227+ do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n

228+ when (mods /= []) (do isetPrompt (mkPrompt mods))

229+ ideslave h orig mods

230+

231+getNChar :: Handle -> Int -> String -> IO (String)

232+getNChar _ 0 s = return (reverse s)

233+getNChar h n s = do c <- hGetChar h

234+ getNChar h (n - 1) (c : s)

235+

236+getLen :: Handle -> Idris (Int)

237+getLen h = do s <- runIO $ getNChar h 6 ""

238+ case readHex s of

239+ ((num, ""):_) -> return num

240+ _ -> ierror (Msg $ "Couldn't read length " ++ s)

241+

242+ideslave :: Handle -> IState -> [FilePath] -> Idris ()

243+ideslave h orig mods

221244 = do idrisCatch

222− (do l <- runIO $ getLine

245+ (do let inh = if h == stdout then stdin else h

246+ len <- getLen inh

247+ l <- runIO $ getNChar inh len ""

223248 (sexp, id) <- case IdeSlave.parseMessage l of

224249 Left err -> ierror err

225250 Right (sexp, id) -> return (sexp, id)

226251 i <- getIState

227− putIState $ i { idris_outputmode = (IdeSlave id) }

252+ putIState $ i { idris_outputmode = (IdeSlave id h) }

228253 idrisCatch -- to report correct id back!

229254 (do let fn = case mods of

230255 (f:_) -> f

231− _ -> ""

256+ _ -> ""

232257 case IdeSlave.sexpToCommand sexp of

233− Just cmd -> runIdeSlaveCommand id orig fn mods cmd

258+ Just cmd -> runIdeSlaveCommand h id orig fn mods cmd

234259 Nothing -> iPrintError "did not understand" )

235260 (\e -> do iPrintError $ show e))

236261 (\e -> do iPrintError $ show e)

237− ideslave orig mods

262+ ideslave h orig mods

238263

239264-- | Run IDESlave commands

240−runIdeSlaveCommand :: Integer -- ^^ The continuation ID for the client

265+runIdeSlaveCommand :: Handle -- ^^ The handle for communication

266+ -> Integer -- ^^ The continuation ID for the client

241267 -> IState -- ^^ The original IState

242268 -> FilePath -- ^^ The current open file

243269 -> [FilePath] -- ^^ The currently loaded modules

244270 -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

245271 -> Idris ()

246−runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

272+runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

247273 do c <- colourise

248274 i <- getIState

249275 case parseCmd i "(input)" cmd of

@@ -253,8 +279,8 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

253279 (do process stdout fn (Prove n')

254280 isetPrompt (mkPrompt mods)

255281 case idris_outputmode i of

256− IdeSlave n -> -- signal completion of proof to ide

257− runIO . hPutStrLn stdout $

282+ IdeSlave n h -> -- signal completion of proof to ide

283+ runIO . hPutStrLn h $

258284 IdeSlave.convSExp "return"

259285 (IdeSlave.SymbolAtom "ok", "")

260286 n

@@ -262,25 +288,25 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Interpret cmd) =

262288 (\e -> do ist <- getIState

263289 isetPrompt (mkPrompt mods)

264290 case idris_outputmode i of

265− IdeSlave n ->

266− runIO . hPutStrLn stdout $

291+ IdeSlave n h ->

292+ runIO . hPutStrLn h $

267293 IdeSlave.convSExp "abandon-proof" "Abandoned" n

268294 _ -> return ()

269− ihRenderError stdout $ pprintErr ist e)

295+ ihRenderError h $ pprintErr ist e)

270296 Success cmd -> idrisCatch

271297 (ideslaveProcess fn cmd)

272− (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

273−runIdeSlaveCommand id orig fn mods (IdeSlave.REPLCompletions str) =

298+ (\e -> getIState >>= ihRenderError h . flip pprintErr e)

299+runIdeSlaveCommand h id orig fn mods (IdeSlave.REPLCompletions str) =

274300 do (unused, compls) <- replCompletion (reverse str, "")

275301 let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

276302 IdeSlave.toSExp (map replacement compls,

277303 reverse unused)]

278− runIO $ putStrLn $ IdeSlave.convSExp "return" good id

279−runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

304+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id

305+runIdeSlaveCommand h id orig fn mods (IdeSlave.LoadFile filename toline) =

280306 do i <- getIState

281307 clearErr

282308 putIState (orig { idris_options = idris_options i,

283− idris_outputmode = (IdeSlave id) })

309+ idris_outputmode = (IdeSlave id h) })

284310 loadInputs stdout [filename] toline

285311 isetPrompt (mkPrompt [filename])

286312 -- Report either success or failure

@@ -291,10 +317,10 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.LoadFile filename toline) =

291317 (\fc -> IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

292318 IdeSlave.toSExp fc])

293319 (idris_parsedSpan i)

294− in runIO . putStrLn $ IdeSlave.convSExp "return" msg id

320+ in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

295321 Just x -> iPrintError $ "didn't load " ++ filename

296− ideslave orig [filename]

297−runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

322+ ideslave h orig [filename]

323+runIdeSlaveCommand h id orig fn mods (IdeSlave.TypeOf name) =

298324 case splitName name of

299325 Left err -> iPrintError err

300326 Right n -> process stdout "(ideslave)"

@@ -304,32 +330,32 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

304330 [] -> Left ("Didn't understand name '" ++ s ++ "'")

305331 [n] -> Right $ sUN n

306332 (n:ns) -> Right $ sNS (sUN n) ns

307−runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

333+runIdeSlaveCommand h id orig fn mods (IdeSlave.DocsFor name) =

308334 case parseConst orig name of

309335 Success c -> process stdout "(ideslave)" (DocStr (Right c))

310336 Failure _ ->

311337 case splitName name of

312338 Left err -> iPrintError err

313339 Right n -> process stdout "(ideslave)" (DocStr (Left n))

314−runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

340+runIdeSlaveCommand h id orig fn mods (IdeSlave.CaseSplit line name) =

315341 process stdout fn (CaseSplitAt False line (sUN name))

316−runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

342+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddClause line name) =

317343 process stdout fn (AddClauseFrom False line (sUN name))

318−runIdeSlaveCommand id orig fn mods (IdeSlave.AddProofClause line name) =

344+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddProofClause line name) =

319345 process stdout fn (AddProofClauseFrom False line (sUN name))

320−runIdeSlaveCommand id orig fn mods (IdeSlave.AddMissing line name) =

346+runIdeSlaveCommand h id orig fn mods (IdeSlave.AddMissing line name) =

321347 process stdout fn (AddMissing False line (sUN name))

322−runIdeSlaveCommand id orig fn mods (IdeSlave.MakeWithBlock line name) =

348+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeWithBlock line name) =

323349 process stdout fn (MakeWith False line (sUN name))

324−runIdeSlaveCommand id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

350+runIdeSlaveCommand h id orig fn mods (IdeSlave.ProofSearch r line name hints depth) =

325351 doProofSearch stdout fn False r line (sUN name) (map sUN hints) depth

326−runIdeSlaveCommand id orig fn mods (IdeSlave.MakeLemma line name) =

352+runIdeSlaveCommand h id orig fn mods (IdeSlave.MakeLemma line name) =

327353 case splitName name of

328354 Left err -> iPrintError err

329355 Right n -> process stdout fn (MakeLemma False line n)

330−runIdeSlaveCommand id orig fn mods (IdeSlave.Apropos a) =

356+runIdeSlaveCommand h id orig fn mods (IdeSlave.Apropos a) =

331357 process stdout fn (Apropos a)

332−runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

358+runIdeSlaveCommand h id orig fn mods (IdeSlave.GetOpts) =

333359 do ist <- getIState

334360 let opts = idris_options ist

335361 let impshow = opt_showimp opts

@@ -337,16 +363,16 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.GetOpts) =

337363 let options = (IdeSlave.SymbolAtom "ok",

338364 [(IdeSlave.SymbolAtom "show-implicits", impshow),

339365 (IdeSlave.SymbolAtom "error-context", errCtxt)])

340− runIO . putStrLn $ IdeSlave.convSExp "return" options id

341−runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

366+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id

367+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ShowImpl b) =

342368 do setImpShow b

343369 let msg = (IdeSlave.SymbolAtom "ok", b)

344− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

345−runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

370+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

371+runIdeSlaveCommand h id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

346372 do setErrContext b

347373 let msg = (IdeSlave.SymbolAtom "ok", b)

348− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

349−runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

374+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

375+runIdeSlaveCommand h id orig fn mods (IdeSlave.Metavariables cols) =

350376 do ist <- getIState

351377 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

352378 let ppo = ppOptionIst ist

@@ -362,7 +388,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

362388 (zip bnds hs),

363389 render ist bnd c pc))

364390 splitMvs

365− runIO . putStrLn $

391+ runIO . hPutStrLn h $

366392 IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id

367393 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)

368394 mapSnd f xs = zip (map fst xs) (map (f . snd) xs)

@@ -407,32 +433,32 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

407433 let (out, spans) = render ist bnd t pt in

408434 (show n , out, spans)

409435

410−runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

436+runIdeSlaveCommand h id orig fn mods (IdeSlave.WhoCalls n) =

411437 case splitName n of

412438 Left err -> iPrintError err

413439 Right n -> do calls <- whoCalls n

414440 ist <- getIState

415441 let msg = (IdeSlave.SymbolAtom "ok",

416442 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

417− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

443+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

418444 where pn ist = displaySpans .

419445 renderPretty 0.9 1000 .

420446 fmap (fancifyAnnots ist) .

421447 prettyName True True []

422−runIdeSlaveCommand id orig fn mods (IdeSlave.CallsWho n) =

448+runIdeSlaveCommand h id orig fn mods (IdeSlave.CallsWho n) =

423449 case splitName n of

424450 Left err -> iPrintError err

425451 Right n -> do calls <- callsWho n

426452 ist <- getIState

427453 let msg = (IdeSlave.SymbolAtom "ok",

428454 map (\ (n,ns) -> (pn ist n, map (pn ist) ns)) calls)

429− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

455+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

430456 where pn ist = displaySpans .

431457 renderPretty 0.9 1000 .

432458 fmap (fancifyAnnots ist) .

433459 prettyName True True []

434460

435−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

461+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

436462 do ctxt <- getContext

437463 ist <- getIState

438464 let tm' = force (normaliseAll ctxt [] tm)

@@ -446,15 +472,15 @@ runIdeSlaveCommand id orig fn modes (IdeSlave.TermNormalise bnd tm) =

446472 displaySpans .

447473 renderPretty 0.9 80 .

448474 fmap (fancifyAnnots ist) $ ptm)

449− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

450−runIdeSlaveCommand id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

451− ideSlaveForceTermImplicits id bnd True tm

452−runIdeSlaveCommand id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

453− ideSlaveForceTermImplicits id bnd False tm

475+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

476+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermShowImplicits bnd tm) =

477+ ideSlaveForceTermImplicits h id bnd True tm

478+runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNoImplicits bnd tm) =

479+ ideSlaveForceTermImplicits h id bnd False tm

454480

455481-- | Show a term for IDESlave with the specified implicitness

456−ideSlaveForceTermImplicits :: Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

457−ideSlaveForceTermImplicits id bnd impl tm =

482+ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

483+ideSlaveForceTermImplicits h id bnd impl tm =

458484 do ist <- getIState

459485 let expl = annotate (AnnTerm bnd tm)

460486 (pprintPTerm ((ppOptionIst ist) { ppopt_impl = impl })

@@ -464,7 +490,7 @@ ideSlaveForceTermImplicits id bnd impl tm =

464490 displaySpans .

465491 renderPretty 0.9 80 .

466492 fmap (fancifyAnnots ist) $ expl)

467− runIO . putStrLn $ IdeSlave.convSExp "return" msg id

493+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

468494

469495splitName :: String -> Either String Name

470496splitName s = case reverse $ splitOn "." s of

@@ -950,8 +976,8 @@ process h fn Execute

950976 case idris_outputmode ist of

951977 RawOutput -> do runIO $ system tmpn

952978 return ()

953− IdeSlave n -> runIO . hPutStrLn h $

954− IdeSlave.convSExp "run-program" tmpn n)

979+ IdeSlave n h -> runIO . hPutStrLn h $

980+ IdeSlave.convSExp "run-program" tmpn n)

955981 (\e -> getIState >>= ihRenderError stdout . flip pprintErr e)

956982 where fc = fileFC "main"

957983process h fn (Compile codegen f)

@@ -1275,7 +1301,6 @@ idrisMain opts =

12751301 mapM_ addLangExt (opt getLanguageExt opts)

12761302 setREPL runrepl

12771303 setQuiet (quiet || isJust script || not (null immediate))

1278− setIdeSlave idesl

12791304 setVerbose verbose

12801305 setCmdLine opts

12811306 setOutputTy outty

@@ -1359,7 +1384,8 @@ idrisMain opts =

13591384-- clearOrigPats

13601385 startServer orig inputs

13611386 runInputT (replSettings (Just historyFile)) $ repl orig inputs

1362− when (idesl) $ ideslaveStart orig inputs

1387+ let idesock = IdeslaveSocket `elem` opts

1388+ when (idesl) $ ideslaveStart idesock orig inputs

13631389 ok <- noErrors

13641390 when (not ok) $ runIO (exitWith (ExitFailure 1))

13651391 where

src/Idris/TypeSearch.hs+3−3

@@ -50,9 +50,9 @@ searchByType h pterm = do

5050 displayScore score <> char ' ' <> prettyDocumentedIst i docInfo

5151 | (n, score) <- names']

5252 case idris_outputmode i of

53− RawOutput -> do mapM_ (ihRenderOutput h) docs

54− ihPrintResult h ""

55− IdeSlave n -> ihRenderResult h (vsep docs)

53+ RawOutput -> do mapM_ (ihRenderOutput h) docs

54+ ihPrintResult h ""

55+ IdeSlave n h -> ihRenderResult h (vsep docs)

5656 where

5757 numLimit = 50

5858 syn = defaultSyntax { implicitAllowed = True } -- syntax