807d623 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1912 from david-christiansen/ide-mode

807d623David Christiansen12 years ago

CHANGELOG+5

compare with master

unifiedsplit

@@ -1,3 +1,8 @@

1+New in 0.9.17:

2+--------------

3+* The --ideslave command line option has been replaced with a --ide-mode

4+ command line option with the same semantics.

1New in 0.9.16:

6New in 0.9.16:

2--------------

7--------------

3* Inductive-inductive definitions are now supported (i.e. simultaneously

8* Inductive-inductive definitions are now supported (i.e. simultaneously

idris.cabal+1−1

@@ -682,7 +682,7 @@ Library

682 , Idris.ErrReverse

683 , Idris.Help

684 , Idris.IBC

685− , Idris.IdeSlave

685+ , Idris.IdeMode

686 , Idris.IdrisDoc

687 , Idris.Imports

688 , Idris.Inliner

src/Idris/AbsSyntax.hs+10−8

@@ -10,7 +10,7 @@ import Idris.Core.Typecheck

10import Idris.AbsSyntaxTree

11import Idris.Colours

12import Idris.Docstrings

13−import Idris.IdeSlave hiding (Opt(..))

13+import Idris.IdeMode hiding (Opt(..))

14import IRTS.CodegenCommon

15import Util.DynamicLinker

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

601isetPrompt :: String -> Idris ()

602isetPrompt p = do i <- getIState

603 case idris_outputmode i of

604− IdeSlave n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

604+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "set-prompt" p n

605

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

607isetLoadedRegion :: Idris ()

@@ -610,7 +610,7 @@ isetLoadedRegion = do i <- getIState

610 case span of

611 Just fc ->

612 case idris_outputmode i of

613− IdeSlave n h ->

613+ IdeMode n h ->

614 runIO . hPutStrLn h $

615 convSExp "set-loaded-region" fc n

616 Nothing -> return ()

@@ -752,10 +752,12 @@ outputTy :: Idris OutputType

752outputTy = do i <- getIState

753 return $ opt_outputTy $ idris_options i

754

755−setIdeSlave :: Bool -> Handle -> Idris ()

755+setIdeMode :: Bool -> Handle -> Idris ()

756−setIdeSlave True h = do i <- getIState

756+setIdeMode True h = do i <- getIState

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

757+ putIState $ i { idris_outputmode = IdeMode 0 h

758+ , idris_colourRepl = False

759+ }

758−setIdeSlave False _ = return ()

760+setIdeMode False _ = return ()

759

761

760setTargetTriple :: String -> Idris ()

762setTargetTriple :: String -> Idris ()

761setTargetTriple t = do i <- getIState

763setTargetTriple t = do i <- getIState

@@ -870,7 +872,7 @@ logLvl l str = do i <- getIState

870 when (lvl >= l) $

872 when (lvl >= l) $

871 case idris_outputmode i of

873 case idris_outputmode i of

872 RawOutput h -> do runIO $ hPutStrLn h str

874 RawOutput h -> do runIO $ hPutStrLn h str

873− IdeSlave n h ->

875+ IdeMode n h ->

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

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

875 runIO . hPutStrLn h $ convSExp "log" good n

877 runIO . hPutStrLn h $ convSExp "log" good n

876

878

src/Idris/AbsSyntaxTree.hs+3−3

@@ -144,7 +144,7 @@ data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord

144

145-- | The output mode in use

146data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle

147− | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle

147+ | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle

148 deriving Show

149

150-- | How wide is the console?

@@ -405,8 +405,8 @@ data Opt = Filename String

405 | Quiet

406 | NoBanner

407 | ColourREPL Bool

408− | Ideslave

408+ | Idemode

409− | IdeslaveSocket

409+ | IdemodeSocket

410 | ShowLibs

411 | ShowLibdir

412 | ShowIncs

src/Idris/CmdOptions.hs+4−2

@@ -71,8 +71,10 @@ parseFlags :: Parser [Opt]

71parseFlags = many $

72 flag' NoBanner (long "nobanner" <> help "Suppress the banner")

73 <|> flag' Quiet (short 'q' <> long "quiet" <> help "Quiet verbosity")

74− <|> flag' Ideslave (long "ideslave")

74+ <|> flag' Idemode (long "ide-mode" <> help "Run the Idris REPL with machine-readable syntax")

75− <|> flag' IdeslaveSocket (long "ideslave-socket")

75+ <|> flag' IdemodeSocket (long "ide-mode-socket" <> help "Choose a socket for IDE mode to listen on")

76+ <|> flag' Idemode (long "ideslave" <> help "Deprecated version of --ide-mode") -- TODO: Remove in v0.9.18

77+ <|> flag' IdemodeSocket (long "ideslave-socket" <> help "Deprecated version of --ide-mode-socket") -- TODO: Remove in v0.9.18

76 <|> (Client <$> strOption (long "client"))

78 <|> (Client <$> strOption (long "client"))

77 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

79 <|> (OLogging <$> option auto (long "log" <> metavar "LEVEL" <> help "Debugging log level"))

78 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

80 <|> flag' NoBasePkgs (long "nobasepkgs" <> help "Do not use the given base package")

src/Idris/IdeSlave.hs → src/Idris/IdeMode.hsrenamed+29−29

@@ -2,7 +2,7 @@

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

5−module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

5+module Idris.IdeMode(parseMessage, convSExp, IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar) where

7import Text.Printf

8import Numeric

@@ -206,32 +206,32 @@ parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

206

207data Opt = ShowImpl | ErrContext deriving Show

208

209−data IdeSlaveCommand = REPLCompletions String

209+data IdeModeCommand = REPLCompletions String

210− | Interpret String

210+ | Interpret String

211− | TypeOf String

211+ | TypeOf String

212− | CaseSplit Int String

212+ | CaseSplit Int String

213− | AddClause Int String

213+ | AddClause Int String

214− | AddProofClause Int String

214+ | AddProofClause Int String

215− | AddMissing Int String

215+ | AddMissing Int String

216− | MakeWithBlock Int String

216+ | MakeWithBlock Int String

217− | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

217+ | ProofSearch Bool Int String [String] (Maybe Int) -- ^^ Recursive?, line, name, hints, depth

218− | MakeLemma Int String

218+ | MakeLemma Int String

219− | LoadFile String (Maybe Int)

219+ | LoadFile String (Maybe Int)

220− | DocsFor String

220+ | DocsFor String

221− | Apropos String

221+ | Apropos String

222− | GetOpts

222+ | GetOpts

223− | SetOpt Opt Bool

223+ | SetOpt Opt Bool

224− | Metavariables Int -- ^^ the Int is the column count for pretty-printing

224+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing

225− | WhoCalls String

225+ | WhoCalls String

226− | CallsWho String

226+ | CallsWho String

227− | TermNormalise [(Name, Bool)] Term

227+ | TermNormalise [(Name, Bool)] Term

228− | TermShowImplicits [(Name, Bool)] Term

228+ | TermShowImplicits [(Name, Bool)] Term

229− | TermNoImplicits [(Name, Bool)] Term

229+ | TermNoImplicits [(Name, Bool)] Term

230− | PrintDef String

230+ | PrintDef String

231− | ErrString Err

231+ | ErrString Err

232− | ErrPPrint Err

232+ | ErrPPrint Err

233−

233+

234−sexpToCommand :: SExp -> Maybe IdeSlaveCommand

234+sexpToCommand :: SExp -> Maybe IdeModeCommand

235sexpToCommand (SexpList (x:[])) = sexpToCommand x

236sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

237sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

@@ -298,5 +298,5 @@ convSExp pre s id =

298getHexLength :: String -> String

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

300

301−ideSlaveEpoch :: Int

301+ideModeEpoch :: Int

302−ideSlaveEpoch = 1

302+ideModeEpoch = 1

src/Idris/Interactive.hs+3−3

@@ -16,7 +16,7 @@ import Idris.ElabTerm

16import Idris.Error

17import Idris.Delaborate

18import Idris.Output

19−import Idris.IdeSlave hiding (IdeSlaveCommand(..))

19+import Idris.IdeMode hiding (IdeModeCommand(..))

21import Idris.Elab.Value

@@ -271,7 +271,7 @@ makeLemma fn updatefile l n

271 runIO $ copyFile fb fn

272 else case idris_outputmode i of

273 RawOutput _ -> iPrintResult $ lem ++ "\n" ++ lem_app

274− IdeSlave n h ->

274+ IdeMode n h ->

275 let good = SexpList [SymbolAtom "ok",

276 SexpList [SymbolAtom "metavariable-lemma",

277 SexpList [SymbolAtom "replace-metavariable",

@@ -289,7 +289,7 @@ makeLemma fn updatefile l n

289 runIO $ copyFile fb fn

290 else case idris_outputmode i of

291 RawOutput _ -> iPrintResult $ lem_app

292− IdeSlave n h ->

292+ IdeMode n h ->

293 let good = SexpList [SymbolAtom "ok",

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

295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+18−18

@@ -8,7 +8,7 @@ import Idris.Core.Evaluate (isDConName, isTConName, isFnName, normaliseAll)

8import Idris.AbsSyntax

9import Idris.Delaborate

10import Idris.Docstrings

11−import Idris.IdeSlave

11+import Idris.IdeMode

13import Util.Pretty

14import Util.ScreenSize (getScreenWidth)

@@ -43,7 +43,7 @@ iWarn fc err =

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

44 else err

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

46− IdeSlave n h ->

46+ IdeMode n h ->

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

48 let (str, spans) = displaySpans err'

49 runIO . hPutStrLn h $

@@ -52,8 +52,8 @@ iWarn fc err =

52iRender :: Doc a -> Idris (SimpleDoc a)

53iRender d = do w <- getWidth

54 ist <- getIState

55− let ideSlave = case idris_outputmode ist of

55+ let ideMode = case idris_outputmode ist of

56− IdeSlave _ _ -> True

56+ IdeMode _ _ -> True

57 _ -> False

58 case w of

59 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

@@ -61,7 +61,7 @@ iRender d = do w <- getWidth

61 if n < 1

62 then renderPretty 1.0 1000000000 d

63 else renderPretty 0.8 n d

64− AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

64+ AutomaticWidth | ideMode -> return $ renderPretty 1.0 1000000000 d

65 | otherwise -> do width <- runIO getScreenWidth

66 return $ renderPretty 0.8 width d

@@ -76,7 +76,7 @@ consoleDisplayAnnotated h output = do ist <- getIState

76iPrintTermWithType :: Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

77iPrintTermWithType tm ty = iRenderResult (tm <+> colon <+> align ty)

79−-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

79+-- | Pretty-print a collection of overloadings to REPL or IDEMode - corresponds to :t name

80iPrintFunTypes :: [(Name, Bool)] -> Name -> [(Name, Doc OutputAnnotation)] -> Idris ()

81iPrintFunTypes bnd n [] = iPrintError $ "No such variable " ++ show n

82iPrintFunTypes bnd n overloads = do ist <- getIState

@@ -94,7 +94,7 @@ iRenderOutput doc =

94 case idris_outputmode i of

95 RawOutput h -> do out <- iRender doc

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

97− IdeSlave n h ->

97+ IdeMode n h ->

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

99 let out = [toSExp str, toSExp spans]

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

@@ -103,10 +103,10 @@ iRenderResult :: Doc OutputAnnotation -> Idris ()

103iRenderResult d = do ist <- getIState

104 case idris_outputmode ist of

105 RawOutput h -> consoleDisplayAnnotated h d

106− IdeSlave n h -> ideSlaveReturnAnnotated n h d

106+ IdeMode n h -> ideModeReturnAnnotated n h d

107

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

108+ideModeReturnWithStatus :: String -> Integer -> Handle -> Doc OutputAnnotation -> Idris ()

109−ideSlaveReturnWithStatus status n h out = do

109+ideModeReturnWithStatus status n h out = do

110 ist <- getIState

111 (str, spans) <- fmap displaySpans .

112 iRender .

@@ -116,16 +116,16 @@ ideSlaveReturnWithStatus status n h out = do

116 runIO . hPutStrLn h $ convSExp "return" good n

117

118

119−-- | Write pretty-printed output to IDESlave with semantic annotations

119+-- | Write pretty-printed output to IDEMode with semantic annotations

120−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

120+ideModeReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

121−ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

121+ideModeReturnAnnotated = ideModeReturnWithStatus "ok"

122

123-- | Show an error with semantic highlighting

124iRenderError :: Doc OutputAnnotation -> Idris ()

125iRenderError e = do ist <- getIState

126 case idris_outputmode ist of

127 RawOutput h -> consoleDisplayAnnotated h e

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

128+ IdeMode n h -> ideModeReturnWithStatus "error" n h e

129

130iPrintWithStatus :: String -> String -> Idris ()

131iPrintWithStatus status s = do

@@ -134,7 +134,7 @@ iPrintWithStatus status s = do

134 RawOutput h -> case s of

135 "" -> return ()

136 s -> runIO $ hPutStrLn h s

137− IdeSlave n h ->

137+ IdeMode n h ->

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

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

140

@@ -149,13 +149,13 @@ iputStrLn :: String -> Idris ()

149iputStrLn s = do i <- getIState

150 case idris_outputmode i of

151 RawOutput h -> runIO $ hPutStrLn h s

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

152+ IdeMode n h -> runIO . hPutStrLn h $ convSExp "write-string" s n

153

154

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

156ideslavePutSExp cmd info = do i <- getIState

157 case idris_outputmode i of

158− IdeSlave n h -> runIO . hPutStrLn h $ convSExp cmd info n

158+ IdeMode n h -> runIO . hPutStrLn h $ convSExp cmd info n

159 _ -> return ()

160

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

@@ -163,7 +163,7 @@ iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

163iputGoal g = do i <- getIState

164 case idris_outputmode i of

165 RawOutput h -> runIO $ hPutStrLn h (displayDecorated (consoleDecorate i) g)

166− IdeSlave n h ->

166+ IdeMode n h ->

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

168 goal = [toSExp str, toSExp spans]

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

src/Idris/Parser.hs+1−1

@@ -1192,7 +1192,7 @@ parseProg syn fname input mrk

1192 i <- getIState

1193 case idris_outputmode i of

1194 RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc)

1195− IdeSlave n h -> iWarn fc (P.text msg)

1195+ IdeMode n h -> iWarn fc (P.text msg)

1196 putIState (i { errSpan = Just fc })

1197 return []

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

src/Idris/Prover.hs+15−15

@@ -20,7 +20,7 @@ import Idris.Parser hiding (params)

20import Idris.Error

21import Idris.DataOpts

22import Idris.Completion

23−import qualified Idris.IdeSlave as IdeSlave

23+import qualified Idris.IdeMode as IdeMode

24import Idris.Output

25import Idris.TypeSearch (searchByType)

@@ -72,7 +72,7 @@ prove opt ctxt lit n ty

72 iLOG $ "Adding " ++ show tm

73 i <- getIState

74 case idris_outputmode i of

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

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

76 _ -> iputStrLn $ showProof lit n prf

77 let proofs = proof_list i

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

@@ -95,8 +95,8 @@ prove opt ctxt lit n ty

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

96 solveDeferred n

97 case idris_outputmode i of

98− IdeSlave n h ->

98+ IdeMode n h ->

99− runIO . hPutStrLn h $ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", "") n

99+ runIO . hPutStrLn h $ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", "") n

100 _ -> return ()

101

102elabStep :: ElabState EState -> ElabD a -> Idris (a, ElabState EState)

@@ -185,24 +185,24 @@ receiveInput :: Handle -> ElabState EState -> Idris (Maybe String)

185receiveInput h e =

186 do i <- getIState

187 let inh = if h == stdout then stdin else h

188− len' <- runIO $ IdeSlave.getLen inh

188+ len' <- runIO $ IdeMode.getLen inh

189 len <- case len' of

190 Left err -> ierror err

191 Right n -> return n

192− l <- runIO $ IdeSlave.getNChar inh len ""

192+ l <- runIO $ IdeMode.getNChar inh len ""

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

193+ (sexp, id) <- case IdeMode.parseMessage l of

194 Left err -> ierror err

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

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

196+ putIState $ i { idris_outputmode = (IdeMode id h) }

197− case IdeSlave.sexpToCommand sexp of

197+ case IdeMode.sexpToCommand sexp of

198− Just (IdeSlave.REPLCompletions prefix) ->

198+ Just (IdeMode.REPLCompletions prefix) ->

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

200− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok", IdeSlave.toSExp (map replacement compls, reverse unused)]

200+ let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok", IdeMode.toSExp (map replacement compls, reverse unused)]

201 ideslavePutSExp "return" good

202 receiveInput h e

203− Just (IdeSlave.Interpret cmd) -> return (Just cmd)

203+ Just (IdeMode.Interpret cmd) -> return (Just cmd)

204− Just (IdeSlave.TypeOf str) -> return (Just (":t " ++ str))

204+ Just (IdeMode.TypeOf str) -> return (Just (":t " ++ str))

205− Just (IdeSlave.DocsFor str) -> return (Just (":doc " ++ str))

205+ Just (IdeMode.DocsFor str) -> return (Just (":doc " ++ str))

206 _ -> return Nothing

207

208ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History -> Idris (Term, [String])

@@ -221,7 +221,7 @@ ploop fn d prompt prf e h

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

222 h' <- getHistory

223 return (l, Just h')

224− IdeSlave _ handle ->

224+ IdeMode _ handle ->

225 do isetPrompt prompt

226 i <- receiveInput handle e

227 return (i, h)

src/Idris/REPL.hs+89−89

@@ -22,7 +22,7 @@ import Idris.Primitives

22import Idris.Coverage

23import Idris.Docs hiding (Doc)

24import Idris.Completion

25−import qualified Idris.IdeSlave as IdeSlave

25+import qualified Idris.IdeMode as IdeMode

26import Idris.Chaser

27import Idris.Imports

28import Idris.Colours hiding (colourise)

@@ -165,7 +165,7 @@ startServer port orig fn_in = do tid <- runIO $ forkOS (serverLoop port)

165 cmd <- hGetLine h

166 let isth = case idris_outputmode ist of

167 RawOutput _ -> ist {idris_outputmode = RawOutput h}

168− IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

168+ IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

169 (ist', fn) <- processNetCmd orig isth h fn cmd

170 hClose h

171 loop fn ist' sock

@@ -204,7 +204,7 @@ processNetCmd orig i h fn cmd

204 do ist <- getIState

205 putIState $ case idris_outputmode ist of

206 RawOutput _ -> ist {idris_outputmode = RawOutput h}

207− IdeSlave n _ -> ist {idris_outputmode = IdeSlave n h}

207+ IdeMode n _ -> ist {idris_outputmode = IdeMode n h}

208

209-- | Run a command on the server on localhost

210runClient :: PortID -> String -> IO ()

@@ -232,25 +232,25 @@ runClient port str = withSocketsDo $ do

232 putStrLn "Unable to connect to a running Idris repl"

233

234

235−initIdeslaveSocket :: IO Handle

235+initIdemodeSocket :: IO Handle

236−initIdeslaveSocket = do

236+initIdemodeSocket = do

237 (sock, port) <- listenOnLocalhostAnyPort

238 putStrLn $ show port

239 (h, _, _) <- accept sock

240 hSetEncoding h utf8

241 return h

242

243−-- | Run the IdeSlave

243+-- | Run the IdeMode

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

245ideslaveStart s orig mods

246− = do h <- runIO $ if s then initIdeslaveSocket else return stdout

246+ = do h <- runIO $ if s then initIdemodeSocket else return stdout

247− setIdeSlave True h

247+ setIdeMode True h

248 i <- getIState

249 case idris_outputmode i of

250− IdeSlave n h ->

250+ IdeMode n h ->

251− do runIO $ hPutStrLn h $ IdeSlave.convSExp "protocol-version" IdeSlave.ideSlaveEpoch n

251+ do runIO $ hPutStrLn h $ IdeMode.convSExp "protocol-version" IdeMode.ideModeEpoch n

252 case mods of

253− a:_ -> runIdeSlaveCommand h n i "" [] (IdeSlave.LoadFile a Nothing)

253+ a:_ -> runIdeModeCommand h n i "" [] (IdeMode.LoadFile a Nothing)

254 _ -> return ()

255 ideslave h orig mods

256

@@ -258,36 +258,36 @@ ideslave :: Handle -> IState -> [FilePath] -> Idris ()

258ideslave h orig mods

259 = do idrisCatch

260 (do let inh = if h == stdout then stdin else h

261− len' <- runIO $ IdeSlave.getLen inh

261+ len' <- runIO $ IdeMode.getLen inh

262 len <- case len' of

263 Left err -> ierror err

264 Right n -> return n

265− l <- runIO $ IdeSlave.getNChar inh len ""

265+ l <- runIO $ IdeMode.getNChar inh len ""

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

266+ (sexp, id) <- case IdeMode.parseMessage l of

267 Left err -> ierror err

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

269 i <- getIState

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

270+ putIState $ i { idris_outputmode = (IdeMode id h) }

271 idrisCatch -- to report correct id back!

272 (do let fn = case mods of

273 (f:_) -> f

274 _ -> ""

275− case IdeSlave.sexpToCommand sexp of

275+ case IdeMode.sexpToCommand sexp of

276− Just cmd -> runIdeSlaveCommand h id orig fn mods cmd

276+ Just cmd -> runIdeModeCommand h id orig fn mods cmd

277 Nothing -> iPrintError "did not understand" )

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

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

280 ideslave h orig mods

281

282−-- | Run IDESlave commands

282+-- | Run IDEMode commands

283−runIdeSlaveCommand :: Handle -- ^^ The handle for communication

283+runIdeModeCommand :: Handle -- ^^ The handle for communication

284 -> Integer -- ^^ The continuation ID for the client

285 -> IState -- ^^ The original IState

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

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

288− -> IdeSlave.IdeSlaveCommand -- ^^ The command to process

288+ -> IdeMode.IdeModeCommand -- ^^ The command to process

289 -> Idris ()

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

290+runIdeModeCommand h id orig fn mods (IdeMode.Interpret cmd) =

291 do c <- colourise

292 i <- getIState

293 case parseCmd i "(input)" cmd of

@@ -297,96 +297,96 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.Interpret cmd) =

297 (do process fn (Prove n')

298 isetPrompt (mkPrompt mods)

299 case idris_outputmode i of

300− IdeSlave n h -> -- signal completion of proof to ide

300+ IdeMode n h -> -- signal completion of proof to ide

301 runIO . hPutStrLn h $

302− IdeSlave.convSExp "return"

302+ IdeMode.convSExp "return"

303− (IdeSlave.SymbolAtom "ok", "")

303+ (IdeMode.SymbolAtom "ok", "")

304 n

305 _ -> return ())

306 (\e -> do ist <- getIState

307 isetPrompt (mkPrompt mods)

308 case idris_outputmode i of

309− IdeSlave n h ->

309+ IdeMode n h ->

310 runIO . hPutStrLn h $

311− IdeSlave.convSExp "abandon-proof" "Abandoned" n

311+ IdeMode.convSExp "abandon-proof" "Abandoned" n

312 _ -> return ()

313 iRenderError $ pprintErr ist e)

314 Success (Right cmd) -> idrisCatch

315 (ideslaveProcess fn cmd)

316 (\e -> getIState >>= iRenderError . flip pprintErr e)

317 Success (Left err) -> iPrintError err

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

318+runIdeModeCommand h id orig fn mods (IdeMode.REPLCompletions str) =

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

320− let good = IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

320+ let good = IdeMode.SexpList [IdeMode.SymbolAtom "ok",

321− IdeSlave.toSExp (map replacement compls,

321+ IdeMode.toSExp (map replacement compls,

322 reverse unused)]

323− runIO . hPutStrLn h $ IdeSlave.convSExp "return" good id

323+ runIO . hPutStrLn h $ IdeMode.convSExp "return" good id

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

324+runIdeModeCommand h id orig fn mods (IdeMode.LoadFile filename toline) =

325 do i <- getIState

326 clearErr

327 putIState (orig { idris_options = idris_options i,

328− idris_outputmode = (IdeSlave id h) })

328+ idris_outputmode = (IdeMode id h) })

329 mods <- loadInputs [filename] toline

330 isetPrompt (mkPrompt mods)

331 -- Report either success or failure

332 i <- getIState

333 case (errSpan i) of

334− Nothing -> let msg = maybe (IdeSlave.SexpList [IdeSlave.SymbolAtom "ok",

334+ Nothing -> let msg = maybe (IdeMode.SexpList [IdeMode.SymbolAtom "ok",

335− IdeSlave.SexpList []])

335+ IdeMode.SexpList []])

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

336+ (\fc -> IdeMode.SexpList [IdeMode.SymbolAtom "ok",

337− IdeSlave.toSExp fc])

337+ IdeMode.toSExp fc])

338 (idris_parsedSpan i)

339− in runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

339+ in runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

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

341 ideslave h orig mods

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

342+runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

343 case splitName name of

344 Left err -> iPrintError err

345 Right n -> process "(ideslave)"

346 (Check (PRef (FC "(ideslave)" (0,0) (0,0)) n))

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

347+runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name) =

348 case parseConst orig name of

349 Success c -> process "(ideslave)" (DocStr (Right c))

350 Failure _ ->

351 case splitName name of

352 Left err -> iPrintError err

353 Right n -> process "(ideslave)" (DocStr (Left n))

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

354+runIdeModeCommand h id orig fn mods (IdeMode.CaseSplit line name) =

355 process fn (CaseSplitAt False line (sUN name))

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

356+runIdeModeCommand h id orig fn mods (IdeMode.AddClause line name) =

357 process fn (AddClauseFrom False line (sUN name))

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

358+runIdeModeCommand h id orig fn mods (IdeMode.AddProofClause line name) =

359 process fn (AddProofClauseFrom False line (sUN name))

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

360+runIdeModeCommand h id orig fn mods (IdeMode.AddMissing line name) =

361 process fn (AddMissing False line (sUN name))

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

362+runIdeModeCommand h id orig fn mods (IdeMode.MakeWithBlock line name) =

363 process fn (MakeWith False line (sUN name))

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

364+runIdeModeCommand h id orig fn mods (IdeMode.ProofSearch r line name hints depth) =

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

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

366+runIdeModeCommand h id orig fn mods (IdeMode.MakeLemma line name) =

367 case splitName name of

368 Left err -> iPrintError err

369 Right n -> process fn (MakeLemma False line n)

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

370+runIdeModeCommand h id orig fn mods (IdeMode.Apropos a) =

371 process fn (Apropos [] a)

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

372+runIdeModeCommand h id orig fn mods (IdeMode.GetOpts) =

373 do ist <- getIState

374 let opts = idris_options ist

375 let impshow = opt_showimp opts

376 let errCtxt = opt_errContext opts

377− let options = (IdeSlave.SymbolAtom "ok",

377+ let options = (IdeMode.SymbolAtom "ok",

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

378+ [(IdeMode.SymbolAtom "show-implicits", impshow),

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

379+ (IdeMode.SymbolAtom "error-context", errCtxt)])

380− runIO . hPutStrLn h $ IdeSlave.convSExp "return" options id

380+ runIO . hPutStrLn h $ IdeMode.convSExp "return" options id

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

381+runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ShowImpl b) =

382 do setImpShow b

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

383+ let msg = (IdeMode.SymbolAtom "ok", b)

384− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

384+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

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

385+runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) =

386 do setErrContext b

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

387+ let msg = (IdeMode.SymbolAtom "ok", b)

388− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

388+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

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

389+runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

390 do ist <- getIState

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

392 let ppo = ppOptionIst ist

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

403 render ist bnd c pc))

404 splitMvs

405 runIO . hPutStrLn h $

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

406+ IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id

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

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

409

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

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

448 (show n , out, spans)

449

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

450+runIdeModeCommand h id orig fn mods (IdeMode.WhoCalls n) =

451 case splitName n of

452 Left err -> iPrintError err

453 Right n -> do calls <- whoCalls n

454 ist <- getIState

455− let msg = (IdeSlave.SymbolAtom "ok",

455+ let msg = (IdeMode.SymbolAtom "ok",

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

457− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

457+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

458 where pn ist = displaySpans .

459 renderPretty 0.9 1000 .

460 fmap (fancifyAnnots ist) .

461 prettyName True True []

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

462+runIdeModeCommand h id orig fn mods (IdeMode.CallsWho n) =

463 case splitName n of

464 Left err -> iPrintError err

465 Right n -> do calls <- callsWho n

466 ist <- getIState

467− let msg = (IdeSlave.SymbolAtom "ok",

467+ let msg = (IdeMode.SymbolAtom "ok",

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

469− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

469+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

470 where pn ist = displaySpans .

471 renderPretty 0.9 1000 .

472 fmap (fancifyAnnots ist) .

473 prettyName True True []

474

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

475+runIdeModeCommand h id orig fn modes (IdeMode.TermNormalise bnd tm) =

476 do ctxt <- getContext

477 ist <- getIState

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

@@ -482,46 +482,46 @@ runIdeSlaveCommand h id orig fn modes (IdeSlave.TermNormalise bnd tm) =

482 []

483 (idris_infixes ist)

484 (delab ist tm'))

485− msg = (IdeSlave.SymbolAtom "ok",

485+ msg = (IdeMode.SymbolAtom "ok",

486 displaySpans .

487 renderPretty 0.9 80 .

488 fmap (fancifyAnnots ist) $ ptm)

489− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

489+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

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

490+runIdeModeCommand h id orig fn modes (IdeMode.TermShowImplicits bnd tm) =

491− ideSlaveForceTermImplicits h id bnd True tm

491+ ideModeForceTermImplicits h id bnd True tm

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

492+runIdeModeCommand h id orig fn modes (IdeMode.TermNoImplicits bnd tm) =

493− ideSlaveForceTermImplicits h id bnd False tm

493+ ideModeForceTermImplicits h id bnd False tm

494−runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =

494+runIdeModeCommand h id orig fn mods (IdeMode.PrintDef name) =

495 case splitName name of

496 Left err -> iPrintError err

497 Right n -> process "(ideslave)" (PrintDef n)

498−runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrString e) =

498+runIdeModeCommand h id orig fn modes (IdeMode.ErrString e) =

499 do ist <- getIState

500 let out = displayS . renderPretty 1.0 60 $ pprintErr ist e

501− msg = (IdeSlave.SymbolAtom "ok", IdeSlave.StringAtom $ out "")

501+ msg = (IdeMode.SymbolAtom "ok", IdeMode.StringAtom $ out "")

502− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

502+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

503−runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrPPrint e) =

503+runIdeModeCommand h id orig fn modes (IdeMode.ErrPPrint e) =

504 do ist <- getIState

505 let (out, spans) =

506 displaySpans .

507 renderPretty 0.9 80 .

508 fmap (fancifyAnnots ist) $ pprintErr ist e

509− msg = (IdeSlave.SymbolAtom "ok", out, spans)

509+ msg = (IdeMode.SymbolAtom "ok", out, spans)

510− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

510+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

511

512−-- | Show a term for IDESlave with the specified implicitness

512+-- | Show a term for IDEMode with the specified implicitness

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

513+ideModeForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

514−ideSlaveForceTermImplicits h id bnd impl tm =

514+ideModeForceTermImplicits h id bnd impl tm =

515 do ist <- getIState

516 let expl = annotate (AnnTerm bnd tm)

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

518 bnd [] (idris_infixes ist)

519 (delab ist tm))

520− msg = (IdeSlave.SymbolAtom "ok",

520+ msg = (IdeMode.SymbolAtom "ok",

521 displaySpans .

522 renderPretty 0.9 80 .

523 fmap (fancifyAnnots ist) $ expl)

524− runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

524+ runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id

525

526splitName :: String -> Either String Name

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

@@ -1101,8 +1101,8 @@ process fn Execute

1101 case idris_outputmode ist of

1102 RawOutput h -> do runIO $ rawSystem tmpn []

1103 return ()

1104− IdeSlave n h -> runIO . hPutStrLn h $

1104+ IdeMode n h -> runIO . hPutStrLn h $

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

1105+ IdeMode.convSExp "run-program" tmpn n)

1106 (\e -> getIState >>= iRenderError . flip pprintErr e)

1107 where fc = fileFC "main"

1108process fn (Compile codegen f)

@@ -1487,7 +1487,7 @@ idrisMain opts =

1487 do let inputs = opt getFile opts

1488 let quiet = Quiet `elem` opts

1489 let nobanner = NoBanner `elem` opts

1490− let idesl = Ideslave `elem` opts || IdeslaveSocket `elem` opts

1490+ let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

1491 let runrepl = not (NoREPL `elem` opts)

1492 let verbose = runrepl || Verbose `elem` opts

1493 let output = opt getOutput opts

@@ -1612,7 +1612,7 @@ idrisMain opts =

1612-- clearOrigPats

1613 startServer port orig mods

1614 runInputT (replSettings (Just historyFile)) $ repl orig mods efile

1615− let idesock = IdeslaveSocket `elem` opts

1615+ let idesock = IdemodeSocket `elem` opts

1616 when (idesl) $ ideslaveStart idesock orig inputs

1617 ok <- noErrors

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

src/Idris/TypeSearch.hs+1−1

@@ -57,7 +57,7 @@ searchByType pkgs pterm = do

57 case idris_outputmode i of

58 RawOutput _ -> do mapM_ iRenderOutput docs

59 iPrintResult ""

60− IdeSlave _ _ -> iRenderResult (vsep docs)

60+ IdeMode _ _ -> iRenderResult (vsep docs)

61 putIState i -- don't actually make any changes

62 where

63 numLimit = 50