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

git.iko.soy/Idris-dev

on master help sign in

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

1add7b7Hannes Mehnert12 years ago

src/Idris/AbsSyntax.hs+9−9

compare with master

unifiedsplit

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

537isetPrompt :: String -> Idris ()

538isetPrompt p = do i <- getIState

539 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

541

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

543isetLoadedRegion :: Idris ()

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

546 case span of

547 Just fc ->

548 case idris_outputmode i of

549− IdeSlave n ->

549+ IdeSlave n h ->

550− runIO . putStrLn $

550+ runIO . hPutStrLn h $

551 convSExp "set-loaded-region" fc n

552 Nothing -> return ()

553

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

662outputTy = do i <- getIState

663 return $ opt_outputTy $ idris_options i

664

665−setIdeSlave :: Bool -> Idris ()

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

666−setIdeSlave True = do i <- getIState

666+setIdeSlave True h = do i <- getIState

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

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

668−setIdeSlave False = return ()

668+setIdeSlave False _ = return ()

669

670setTargetTriple :: String -> Idris ()

671setTargetTriple t = do i <- getIState

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

794 when (lvl >= l) $

795 case idris_outputmode i of

796 RawOutput -> do runIO $ putStrLn str

797− IdeSlave n ->

797+ IdeSlave n h ->

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

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

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

800

801cmdOptType :: Opt -> Idris Bool

802cmdOptType x = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1−1

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

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

128

129-- | The output mode in use

130−data OutputMode = RawOutput | IdeSlave Integer deriving Show

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

131

132-- | How wide is the console?

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

src/Idris/IdeSlave.hs+7−10

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

1{-# 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

5import Text.Printf

6import Numeric

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

251

252receiveString :: String -> Either Err SExp

253receiveString 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

254+ case parseSExp x of

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

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

261− Success r -> Right r)

256+ Success r -> Right r

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

263

257

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

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

265convSExp pre s id =

259convSExp pre s id =

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

269

263

270getHexLength :: String -> String

264getHexLength :: String -> String

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

265getHexLength 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

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

267 runIO $ copyFile fb fn

268 else case idris_outputmode i of

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

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

270− IdeSlave n ->

270+ IdeSlave n h ->

271 let good = SexpList [SymbolAtom "ok",

272 SexpList [SymbolAtom "metavariable-lemma",

273 SexpList [SymbolAtom "replace-metavariable",

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

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

285 runIO $ copyFile fb fn

286 else case idris_outputmode i of

287− RawOutput -> ihPrintResult h $ lem_app

287+ RawOutput -> ihPrintResult h $ lem_app

288− IdeSlave n ->

288+ IdeSlave n h ->

289 let good = SexpList [SymbolAtom "ok",

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

291 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+16−16

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

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

34 else err

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

36− IdeSlave n ->

36+ IdeSlave n h ->

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

38 let (str, spans) = displaySpans err'

39 runIO . hPutStrLn h $

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

43iRender d = do w <- getWidth

44 ist <- getIState

45 let ideSlave = case idris_outputmode ist of

46− IdeSlave _ -> True

46+ IdeSlave _ _ -> True

47− _ -> False

47+ _ -> False

48 case w of

49 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

50 ColsWide n -> return $

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

84 case idris_outputmode i of

85 RawOutput -> do out <- iRender doc

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

87− IdeSlave n ->

87+ IdeSlave n h ->

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

89 let out = [toSExp str, toSExp spans]

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

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

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

93ihRenderResult h d = do ist <- getIState

94 case idris_outputmode ist of

95− RawOutput -> consoleDisplayAnnotated h d

95+ RawOutput -> consoleDisplayAnnotated h d

96− IdeSlave n -> ideSlaveReturnAnnotated n h d

96+ IdeSlave n h -> ideSlaveReturnAnnotated n h d

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

99ideSlaveReturnWithStatus status n h out = do

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

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

115ihRenderError h e = do ist <- getIState

116 case idris_outputmode ist of

117− RawOutput -> consoleDisplayAnnotated h e

117+ RawOutput -> consoleDisplayAnnotated h e

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

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

119

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

121−ihPrintWithStatus status h s = do

121+ihPrintWithStatus status h s = do

122 i <- getIState

123 case idris_outputmode i of

124 RawOutput -> case s of

125 "" -> return ()

126 s -> runIO $ hPutStrLn h s

127− IdeSlave n ->

127+ IdeSlave n h ->

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

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

130

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

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

139ihputStrLn h s = do i <- getIState

140 case idris_outputmode i of

141− RawOutput -> runIO $ hPutStrLn h s

141+ RawOutput -> runIO $ hPutStrLn h s

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

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

143

144iputStrLn = ihputStrLn stdout

145iPrintError = ihPrintError stdout

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

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

150ideslavePutSExp cmd info = do i <- getIState

151 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

153 _ -> return ()

154

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

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

157iputGoal g = do i <- getIState

158 case idris_outputmode i of

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

160− IdeSlave n ->

160+ IdeSlave n h ->

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

162 goal = [toSExp str, toSExp spans]

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

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

164

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

166warnTotality :: Idris ()

src/Idris/Parser.hs+2−2

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

1159 let (fc, msg) = findFC doc

1160 i <- getIState

1161 case idris_outputmode i of

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

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

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

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

1164 putIState (i { errSpan = Just fc })

1165 return []

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

src/Idris/Prover.hs+11−11

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

28import System.Console.Haskeline

29import System.Console.Haskeline.History

30+import System.IO (Handle)

30import Control.Monad.State.Strict

31import Control.Monad.State.Strict

31import Control.DeepSeq

32import Control.DeepSeq

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

70 iLOG $ "Adding " ++ show tm

71 iLOG $ "Adding " ++ show tm

71 i <- getIState

72 i <- getIState

72 case idris_outputmode i of

73 case idris_outputmode i of

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

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

74− _ -> iputStrLn $ showProof lit n prf

75+ _ -> iputStrLn $ showProof lit n prf

75 let proofs = proof_list i

76 let proofs = proof_list i

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

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

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

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

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

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

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

94 solveDeferred n

95 solveDeferred n

95 case idris_outputmode i of

96 case idris_outputmode i of

96− IdeSlave n ->

97+ IdeSlave n h ->

97− runIO . putStrLn $

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

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

99 _ -> return ()

100

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

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

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

178 return v

179

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

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

181−receiveInput e =

181+receiveInput e handle =

182 do i <- getIState

183 l <- runIO $ getLine

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

185 Left err -> ierror err

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

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

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

188 case sexpToCommand sexp of

189 Just (REPLCompletions prefix) ->

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

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

192 ideslavePutSExp "return" good

193− receiveInput e

193+ receiveInput e handle

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

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

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

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

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

212 h' <- getHistory

213 return (l, Just h')

214− IdeSlave n ->

214+ IdeSlave _ handle ->

215 do isetPrompt prompt

216− i <- receiveInput e

216+ i <- receiveInput e handle

217 return (i, h)

218 (cmd, step) <- case x of

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

src/Idris/REPL.hs+91−65

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

42import Version_idris (gitHash)

43import Util.System

44import Util.DynamicLinker

45−import Util.Net (listenOnLocalhost)

45+import Util.Net (listenOnLocalhost, listenOnLocalhostAnyPort)

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

48import Idris.Core.Evaluate

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

91import Data.Either (partitionEithers)

92import Control.DeepSeq

94+import Numeric ( readHex )

95+

94import Debug.Trace

96import Debug.Trace

96-- | Run the REPL

98-- | Run the REPL

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

206 else do l <- hGetLine h

208 else do l <- hGetLine h

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

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

208

210

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+

209-- | Run the IdeSlave

219-- | Run the IdeSlave

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

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

211−ideslaveStart orig mods

221+ideslaveStart s orig mods

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

223+ setIdeSlave True h

212− = do i <- getIState

224+ i <- getIState

213 case idris_outputmode i of

225 case idris_outputmode i of

214− IdeSlave n ->

226+ IdeSlave n h ->

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

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

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

216− ideslave orig mods

229+ ideslave h orig mods

217−

230+

218−

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+

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

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

220−ideslave orig mods

243+ideslave h orig mods

221 = do idrisCatch

244 = 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 ""

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

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

224 Left err -> ierror err

249 Left err -> ierror err

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

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

226 i <- getIState

251 i <- getIState

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

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

228 idrisCatch -- to report correct id back!

253 idrisCatch -- to report correct id back!

229 (do let fn = case mods of

254 (do let fn = case mods of

230 (f:_) -> f

255 (f:_) -> f

231− _ -> ""

256+ _ -> ""

232 case IdeSlave.sexpToCommand sexp of

257 case IdeSlave.sexpToCommand sexp of

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

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

234 Nothing -> iPrintError "did not understand" )

259 Nothing -> iPrintError "did not understand" )

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

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

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

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

237− ideslave orig mods

262+ ideslave h orig mods

238

263

239-- | Run IDESlave commands

264-- | Run IDESlave commands

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

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

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

241 -> IState -- ^^ The original IState

267 -> IState -- ^^ The original IState

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

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

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

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

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

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

245 -> Idris ()

271 -> Idris ()

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

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

247 do c <- colourise

273 do c <- colourise

248 i <- getIState

274 i <- getIState

249 case parseCmd i "(input)" cmd of

275 case parseCmd i "(input)" cmd of

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

253 (do process stdout fn (Prove n')

279 (do process stdout fn (Prove n')

254 isetPrompt (mkPrompt mods)

280 isetPrompt (mkPrompt mods)

255 case idris_outputmode i of

281 case idris_outputmode i of

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

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

257− runIO . hPutStrLn stdout $

283+ runIO . hPutStrLn h $

258 IdeSlave.convSExp "return"

284 IdeSlave.convSExp "return"

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

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

260 n

286 n

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

262 (\e -> do ist <- getIState

288 (\e -> do ist <- getIState

263 isetPrompt (mkPrompt mods)

289 isetPrompt (mkPrompt mods)

264 case idris_outputmode i of

290 case idris_outputmode i of

265− IdeSlave n ->

291+ IdeSlave n h ->

266− runIO . hPutStrLn stdout $

292+ runIO . hPutStrLn h $

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

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

268 _ -> return ()

294 _ -> return ()

269− ihRenderError stdout $ pprintErr ist e)

295+ ihRenderError h $ pprintErr ist e)

270 Success cmd -> idrisCatch

296 Success cmd -> idrisCatch

271 (ideslaveProcess fn cmd)

297 (ideslaveProcess fn cmd)

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

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

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

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

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

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

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

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

276 IdeSlave.toSExp (map replacement compls,

302 IdeSlave.toSExp (map replacement compls,

277 reverse unused)]

303 reverse unused)]

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

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

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

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

280 do i <- getIState

306 do i <- getIState

281 clearErr

307 clearErr

282 putIState (orig { idris_options = idris_options i,

308 putIState (orig { idris_options = idris_options i,

283− idris_outputmode = (IdeSlave id) })

309+ idris_outputmode = (IdeSlave id h) })

284 loadInputs stdout [filename] toline

310 loadInputs stdout [filename] toline

285 isetPrompt (mkPrompt [filename])

311 isetPrompt (mkPrompt [filename])

286 -- Report either success or failure

312 -- Report either success or failure

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

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

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

292 IdeSlave.toSExp fc])

318 IdeSlave.toSExp fc])

293 (idris_parsedSpan i)

319 (idris_parsedSpan i)

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

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

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

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

296− ideslave orig [filename]

322+ ideslave h orig [filename]

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

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

298 case splitName name of

324 case splitName name of

299 Left err -> iPrintError err

325 Left err -> iPrintError err

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

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

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

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

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

305 [n] -> Right $ sUN n

331 [n] -> Right $ sUN n

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

332 (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) =

308 case parseConst orig name of

334 case parseConst orig name of

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

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

310 Failure _ ->

336 Failure _ ->

311 case splitName name of

337 case splitName name of

312 Left err -> iPrintError err

338 Left err -> iPrintError err

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

339 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) =

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

341 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) =

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

343 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) =

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

345 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) =

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

347 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) =

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

349 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) =

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

351 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) =

327 case splitName name of

353 case splitName name of

328 Left err -> iPrintError err

354 Left err -> iPrintError err

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

355 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) =

331 process stdout fn (Apropos a)

357 process stdout fn (Apropos a)

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

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

333 do ist <- getIState

359 do ist <- getIState

334 let opts = idris_options ist

360 let opts = idris_options ist

335 let impshow = opt_showimp opts

361 let impshow = opt_showimp opts

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

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

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

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

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

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

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

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

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

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

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

342 do setImpShow b

368 do setImpShow b

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

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

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

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

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

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

346 do setErrContext b

372 do setErrContext b

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

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

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

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

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

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

350 do ist <- getIState

376 do ist <- getIState

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

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

352 let ppo = ppOptionIst ist

378 let ppo = ppOptionIst ist

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

362 (zip bnds hs),

388 (zip bnds hs),

363 render ist bnd c pc))

389 render ist bnd c pc))

364 splitMvs

390 splitMvs

365− runIO . putStrLn $

391+ runIO . hPutStrLn h $

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

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

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

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

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

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

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

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

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

408 (show n , out, spans)

434 (show n , out, spans)

409

435

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

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

411 case splitName n of

437 case splitName n of

412 Left err -> iPrintError err

438 Left err -> iPrintError err

413 Right n -> do calls <- whoCalls n

439 Right n -> do calls <- whoCalls n

414 ist <- getIState

440 ist <- getIState

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

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

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

442 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

418 where pn ist = displaySpans .

444 where pn ist = displaySpans .

419 renderPretty 0.9 1000 .

445 renderPretty 0.9 1000 .

420 fmap (fancifyAnnots ist) .

446 fmap (fancifyAnnots ist) .

421 prettyName True True []

447 prettyName True True []

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

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

423 case splitName n of

449 case splitName n of

424 Left err -> iPrintError err

450 Left err -> iPrintError err

425 Right n -> do calls <- callsWho n

451 Right n -> do calls <- callsWho n

426 ist <- getIState

452 ist <- getIState

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

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

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

454 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

430 where pn ist = displaySpans .

456 where pn ist = displaySpans .

431 renderPretty 0.9 1000 .

457 renderPretty 0.9 1000 .

432 fmap (fancifyAnnots ist) .

458 fmap (fancifyAnnots ist) .

433 prettyName True True []

459 prettyName True True []

434

460

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

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

436 do ctxt <- getContext

462 do ctxt <- getContext

437 ist <- getIState

463 ist <- getIState

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

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

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

446 displaySpans .

472 displaySpans .

447 renderPretty 0.9 80 .

473 renderPretty 0.9 80 .

448 fmap (fancifyAnnots ist) $ ptm)

474 fmap (fancifyAnnots ist) $ ptm)

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

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

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

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

451− ideSlaveForceTermImplicits id bnd True tm

477+ ideSlaveForceTermImplicits h id bnd True tm

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

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

453− ideSlaveForceTermImplicits id bnd False tm

479+ ideSlaveForceTermImplicits h id bnd False tm

454

480

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

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

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

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

457−ideSlaveForceTermImplicits id bnd impl tm =

483+ideSlaveForceTermImplicits h id bnd impl tm =

458 do ist <- getIState

484 do ist <- getIState

459 let expl = annotate (AnnTerm bnd tm)

485 let expl = annotate (AnnTerm bnd tm)

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

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

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

464 displaySpans .

490 displaySpans .

465 renderPretty 0.9 80 .

491 renderPretty 0.9 80 .

466 fmap (fancifyAnnots ist) $ expl)

492 fmap (fancifyAnnots ist) $ expl)

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

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

468

494

469splitName :: String -> Either String Name

495splitName :: String -> Either String Name

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

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

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

950 case idris_outputmode ist of

976 case idris_outputmode ist of

951 RawOutput -> do runIO $ system tmpn

977 RawOutput -> do runIO $ system tmpn

952 return ()

978 return ()

953− IdeSlave n -> runIO . hPutStrLn h $

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

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

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

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

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

956 where fc = fileFC "main"

982 where fc = fileFC "main"

957process h fn (Compile codegen f)

983process h fn (Compile codegen f)

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

1275 mapM_ addLangExt (opt getLanguageExt opts)

1301 mapM_ addLangExt (opt getLanguageExt opts)

1276 setREPL runrepl

1302 setREPL runrepl

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

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

1278− setIdeSlave idesl

1279 setVerbose verbose

1304 setVerbose verbose

1280 setCmdLine opts

1305 setCmdLine opts

1281 setOutputTy outty

1306 setOutputTy outty

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

1359-- clearOrigPats

1384-- clearOrigPats

1360 startServer orig inputs

1385 startServer orig inputs

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

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

1387+ let idesock = IdeslaveSocket `elem` opts

1362− when (idesl) $ ideslaveStart orig inputs

1388+ when (idesl) $ ideslaveStart idesock orig inputs

1363 ok <- noErrors

1389 ok <- noErrors

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

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

1365 where

1391 where

src/Idris/TypeSearch.hs+3−3

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

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

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

52 case idris_outputmode i of

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

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

54− ihPrintResult h ""

54+ ihPrintResult h ""

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

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

56 where

57 numLimit = 50

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