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

git.iko.soy/Idris-dev

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

Rename ideslave to ide-mode

commit807d623a25e670a88995bd58e44ef19a5fe303ba authorDavid Christiansen <david@davidchristiansen.dk> dateThu 12 Feb 2015, 08:51 (12 years ago) parentaa410e4 b85b2eb

12 files changed+179−170

compare with master

unifiedsplit

CHANGELOG+5 idris.cabal+1−1 src/Idris/AbsSyntax.hs+10−8 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/CmdOptions.hs+4−2 src/Idris/IdeSlave.hs → src/Idris/IdeMode.hs+29−29 src/Idris/Interactive.hs+3−3 src/Idris/Output.hs+18−18 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+15−15 src/Idris/REPL.hs+89−89 src/Idris/TypeSearch.hs+1−1

CHANGELOG+5

@@ -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.

16New in 0.9.16:

27--------------

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

idris.cabal+1−1

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

682682 , Idris.ErrReverse

683683 , Idris.Help

684684 , Idris.IBC

685− , Idris.IdeSlave

685+ , Idris.IdeMode

686686 , Idris.IdrisDoc

687687 , Idris.Imports

688688 , Idris.Inliner

src/Idris/AbsSyntax.hs+10−8

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

1010import Idris.AbsSyntaxTree

1111import Idris.Colours

1212import Idris.Docstrings

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

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

1414import IRTS.CodegenCommon

1515import Util.DynamicLinker

1616

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

601601isetPrompt :: String -> Idris ()

602602isetPrompt p = do i <- getIState

603603 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

605605

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

607607isetLoadedRegion :: Idris ()

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

610610 case span of

611611 Just fc ->

612612 case idris_outputmode i of

613− IdeSlave n h ->

613+ IdeMode n h ->

614614 runIO . hPutStrLn h $

615615 convSExp "set-loaded-region" fc n

616616 Nothing -> return ()

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

752752outputTy = do i <- getIState

753753 return $ opt_outputTy $ idris_options i

754754

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

756−setIdeSlave True h = do i <- getIState

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

758−setIdeSlave False _ = return ()

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

756+setIdeMode True h = do i <- getIState

757+ putIState $ i { idris_outputmode = IdeMode 0 h

758+ , idris_colourRepl = False

759+ }

760+setIdeMode False _ = return ()

759761

760762setTargetTriple :: String -> Idris ()

761763setTargetTriple t = do i <- getIState

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

870872 when (lvl >= l) $

871873 case idris_outputmode i of

872874 RawOutput h -> do runIO $ hPutStrLn h str

873− IdeSlave n h ->

875+ IdeMode n h ->

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

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

876878

src/Idris/AbsSyntaxTree.hs+3−3

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

144144

145145-- | The output mode in use

146146data 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

148148 deriving Show

149149

150150-- | How wide is the console?

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

405405 | Quiet

406406 | NoBanner

407407 | ColourREPL Bool

408− | Ideslave

409− | IdeslaveSocket

408+ | Idemode

409+ | IdemodeSocket

410410 | ShowLibs

411411 | ShowLibdir

412412 | ShowIncs

src/Idris/CmdOptions.hs+4−2

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

7171parseFlags = many $

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

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

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

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

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

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

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

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

7880 <|> 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 @@

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

77import Text.Printf

88import Numeric

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

206206

207207data Opt = ShowImpl | ErrContext deriving Show

208208

209−data IdeSlaveCommand = REPLCompletions String

210− | Interpret String

211− | TypeOf String

212− | CaseSplit Int String

213− | AddClause Int String

214− | AddProofClause Int String

215− | AddMissing Int String

216− | MakeWithBlock Int String

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

218− | MakeLemma Int String

219− | LoadFile String (Maybe Int)

220− | DocsFor String

221− | Apropos String

222− | GetOpts

223− | SetOpt Opt Bool

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

225− | WhoCalls String

226− | CallsWho String

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

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

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

230− | PrintDef String

231− | ErrString Err

232− | ErrPPrint Err

233−

234−sexpToCommand :: SExp -> Maybe IdeSlaveCommand

209+data IdeModeCommand = REPLCompletions String

210+ | Interpret String

211+ | TypeOf String

212+ | CaseSplit Int String

213+ | AddClause Int String

214+ | AddProofClause Int String

215+ | AddMissing Int String

216+ | MakeWithBlock Int String

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

218+ | MakeLemma Int String

219+ | LoadFile String (Maybe Int)

220+ | DocsFor String

221+ | Apropos String

222+ | GetOpts

223+ | SetOpt Opt Bool

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

225+ | WhoCalls String

226+ | CallsWho String

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

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

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

230+ | PrintDef String

231+ | ErrString Err

232+ | ErrPPrint Err

233+

234+sexpToCommand :: SExp -> Maybe IdeModeCommand

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

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

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

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

298298getHexLength :: String -> String

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

300300

301−ideSlaveEpoch :: Int

302−ideSlaveEpoch = 1

301+ideModeEpoch :: Int

302+ideModeEpoch = 1

src/Idris/Interactive.hs+3−3

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

1616import Idris.Error

1717import Idris.Delaborate

1818import Idris.Output

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

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

2020

2121import Idris.Elab.Value

2222

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

271271 runIO $ copyFile fb fn

272272 else case idris_outputmode i of

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

274− IdeSlave n h ->

274+ IdeMode n h ->

275275 let good = SexpList [SymbolAtom "ok",

276276 SexpList [SymbolAtom "metavariable-lemma",

277277 SexpList [SymbolAtom "replace-metavariable",

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

289289 runIO $ copyFile fb fn

290290 else case idris_outputmode i of

291291 RawOutput _ -> iPrintResult $ lem_app

292− IdeSlave n h ->

292+ IdeMode n h ->

293293 let good = SexpList [SymbolAtom "ok",

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

295295 SexpList [SymbolAtom "definition-clause",

src/Idris/Output.hs+18−18

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

88import Idris.AbsSyntax

99import Idris.Delaborate

1010import Idris.Docstrings

11−import Idris.IdeSlave

11+import Idris.IdeMode

1212

1313import Util.Pretty

1414import Util.ScreenSize (getScreenWidth)

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

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

4444 else err

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

46− IdeSlave n h ->

46+ IdeMode n h ->

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

4848 let (str, spans) = displaySpans err'

4949 runIO . hPutStrLn h $

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

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

5353iRender d = do w <- getWidth

5454 ist <- getIState

55− let ideSlave = case idris_outputmode ist of

56− IdeSlave _ _ -> True

55+ let ideMode = case idris_outputmode ist of

56+ IdeMode _ _ -> True

5757 _ -> False

5858 case w of

5959 InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

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

6161 if n < 1

6262 then renderPretty 1.0 1000000000 d

6363 else renderPretty 0.8 n d

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

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

6565 | otherwise -> do width <- runIO getScreenWidth

6666 return $ renderPretty 0.8 width d

6767

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

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

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

7878

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

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

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

8282iPrintFunTypes bnd n overloads = do ist <- getIState

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

9494 case idris_outputmode i of

9595 RawOutput h -> do out <- iRender doc

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

97− IdeSlave n h ->

97+ IdeMode n h ->

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

9999 let out = [toSExp str, toSExp spans]

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

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

103103iRenderResult d = do ist <- getIState

104104 case idris_outputmode ist of

105105 RawOutput h -> consoleDisplayAnnotated h d

106− IdeSlave n h -> ideSlaveReturnAnnotated n h d

106+ IdeMode n h -> ideModeReturnAnnotated n h d

107107

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

109−ideSlaveReturnWithStatus status n h out = do

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

109+ideModeReturnWithStatus status n h out = do

110110 ist <- getIState

111111 (str, spans) <- fmap displaySpans .

112112 iRender .

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

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

117117

118118

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

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

121−ideSlaveReturnAnnotated = ideSlaveReturnWithStatus "ok"

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

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

121+ideModeReturnAnnotated = ideModeReturnWithStatus "ok"

122122

123123-- | Show an error with semantic highlighting

124124iRenderError :: Doc OutputAnnotation -> Idris ()

125125iRenderError e = do ist <- getIState

126126 case idris_outputmode ist of

127127 RawOutput h -> consoleDisplayAnnotated h e

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

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

129129

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

131131iPrintWithStatus status s = do

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

134134 RawOutput h -> case s of

135135 "" -> return ()

136136 s -> runIO $ hPutStrLn h s

137− IdeSlave n h ->

137+ IdeMode n h ->

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

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

140140

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

149149iputStrLn s = do i <- getIState

150150 case idris_outputmode i of

151151 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

153153

154154

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

156156ideslavePutSExp cmd info = do i <- getIState

157157 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

159159 _ -> return ()

160160

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

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

163163iputGoal g = do i <- getIState

164164 case idris_outputmode i of

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

166− IdeSlave n h ->

166+ IdeMode n h ->

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

168168 goal = [toSExp str, toSExp spans]

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

src/Idris/Parser.hs+1−1

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

11921192 i <- getIState

11931193 case idris_outputmode i of

11941194 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)

11961196 putIState (i { errSpan = Just fc })

11971197 return []

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

src/Idris/Prover.hs+15−15

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

2020import Idris.Error

2121import Idris.DataOpts

2222import Idris.Completion

23−import qualified Idris.IdeSlave as IdeSlave

23+import qualified Idris.IdeMode as IdeMode

2424import Idris.Output

2525import Idris.TypeSearch (searchByType)

2626

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

7272 iLOG $ "Adding " ++ show tm

7373 i <- getIState

7474 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)

7676 _ -> iputStrLn $ showProof lit n prf

7777 let proofs = proof_list i

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

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

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

9696 solveDeferred n

9797 case idris_outputmode i of

98− IdeSlave n h ->

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

98+ IdeMode n h ->

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

100100 _ -> return ()

101101

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

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

185185receiveInput h e =

186186 do i <- getIState

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

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

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

189189 len <- case len' of

190190 Left err -> ierror err

191191 Right n -> return n

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

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

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

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

194194 Left err -> ierror err

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

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

197− case IdeSlave.sexpToCommand sexp of

198− Just (IdeSlave.REPLCompletions prefix) ->

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

197+ case IdeMode.sexpToCommand sexp of

198+ Just (IdeMode.REPLCompletions prefix) ->

199199 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)]

201201 ideslavePutSExp "return" good

202202 receiveInput h e

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

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

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

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

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

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

206206 _ -> return Nothing

207207

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

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

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

222222 h' <- getHistory

223223 return (l, Just h')

224− IdeSlave _ handle ->

224+ IdeMode _ handle ->

225225 do isetPrompt prompt

226226 i <- receiveInput handle e

227227 return (i, h)

src/Idris/REPL.hs+89−89

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

2222import Idris.Coverage

2323import Idris.Docs hiding (Doc)

2424import Idris.Completion

25−import qualified Idris.IdeSlave as IdeSlave

25+import qualified Idris.IdeMode as IdeMode

2626import Idris.Chaser

2727import Idris.Imports

2828import Idris.Colours hiding (colourise)

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

165165 cmd <- hGetLine h

166166 let isth = case idris_outputmode ist of

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

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

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

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

170170 hClose h

171171 loop fn ist' sock

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

204204 do ist <- getIState

205205 putIState $ case idris_outputmode ist of

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

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

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

208208

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

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

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

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

233233

234234

235−initIdeslaveSocket :: IO Handle

236−initIdeslaveSocket = do

235+initIdemodeSocket :: IO Handle

236+initIdemodeSocket = do

237237 (sock, port) <- listenOnLocalhostAnyPort

238238 putStrLn $ show port

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

240240 hSetEncoding h utf8

241241 return h

242242

243−-- | Run the IdeSlave

243+-- | Run the IdeMode

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

245245ideslaveStart s orig mods

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

247− setIdeSlave True h

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

247+ setIdeMode True h

248248 i <- getIState

249249 case idris_outputmode i of

250− IdeSlave n h ->

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

250+ IdeMode n h ->

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

252252 case mods of

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

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

254254 _ -> return ()

255255 ideslave h orig mods

256256

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

258258ideslave h orig mods

259259 = do idrisCatch

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

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

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

262262 len <- case len' of

263263 Left err -> ierror err

264264 Right n -> return n

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

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

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

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

267267 Left err -> ierror err

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

269269 i <- getIState

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

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

271271 idrisCatch -- to report correct id back!

272272 (do let fn = case mods of

273273 (f:_) -> f

274274 _ -> ""

275− case IdeSlave.sexpToCommand sexp of

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

275+ case IdeMode.sexpToCommand sexp of

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

277277 Nothing -> iPrintError "did not understand" )

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

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

280280 ideslave h orig mods

281281

282−-- | Run IDESlave commands

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

282+-- | Run IDEMode commands

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

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

285285 -> IState -- ^^ The original IState

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

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

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

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

289289 -> Idris ()

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

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

291291 do c <- colourise

292292 i <- getIState

293293 case parseCmd i "(input)" cmd of

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

297297 (do process fn (Prove n')

298298 isetPrompt (mkPrompt mods)

299299 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

301301 runIO . hPutStrLn h $

302− IdeSlave.convSExp "return"

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

302+ IdeMode.convSExp "return"

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

304304 n

305305 _ -> return ())

306306 (\e -> do ist <- getIState

307307 isetPrompt (mkPrompt mods)

308308 case idris_outputmode i of

309− IdeSlave n h ->

309+ IdeMode n h ->

310310 runIO . hPutStrLn h $

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

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

312312 _ -> return ()

313313 iRenderError $ pprintErr ist e)

314314 Success (Right cmd) -> idrisCatch

315315 (ideslaveProcess fn cmd)

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

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

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

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

321− IdeSlave.toSExp (map replacement compls,

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

321+ IdeMode.toSExp (map replacement compls,

322322 reverse unused)]

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

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

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

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

325325 do i <- getIState

326326 clearErr

327327 putIState (orig { idris_options = idris_options i,

328− idris_outputmode = (IdeSlave id h) })

328+ idris_outputmode = (IdeMode id h) })

329329 mods <- loadInputs [filename] toline

330330 isetPrompt (mkPrompt mods)

331331 -- Report either success or failure

332332 i <- getIState

333333 case (errSpan i) of

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

335− IdeSlave.SexpList []])

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

337− IdeSlave.toSExp fc])

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

335+ IdeMode.SexpList []])

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

337+ IdeMode.toSExp fc])

338338 (idris_parsedSpan i)

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

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

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

341341 ideslave h orig mods

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

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

343343 case splitName name of

344344 Left err -> iPrintError err

345345 Right n -> process "(ideslave)"

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

348348 case parseConst orig name of

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

350350 Failure _ ->

351351 case splitName name of

352352 Left err -> iPrintError err

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

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

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

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

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

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

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

367367 case splitName name of

368368 Left err -> iPrintError err

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

371371 process fn (Apropos [] a)

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

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

373373 do ist <- getIState

374374 let opts = idris_options ist

375375 let impshow = opt_showimp opts

376376 let errCtxt = opt_errContext opts

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

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

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

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

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

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

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

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

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

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

382382 do setImpShow b

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

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

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

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

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

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

386386 do setErrContext b

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

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

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

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

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

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

390390 do ist <- getIState

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

392392 let ppo = ppOptionIst ist

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

403403 render ist bnd c pc))

404404 splitMvs

405405 runIO . hPutStrLn h $

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

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

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

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

409409

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

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

448448 (show n , out, spans)

449449

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

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

451451 case splitName n of

452452 Left err -> iPrintError err

453453 Right n -> do calls <- whoCalls n

454454 ist <- getIState

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

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

456456 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

458458 where pn ist = displaySpans .

459459 renderPretty 0.9 1000 .

460460 fmap (fancifyAnnots ist) .

461461 prettyName True True []

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

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

463463 case splitName n of

464464 Left err -> iPrintError err

465465 Right n -> do calls <- callsWho n

466466 ist <- getIState

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

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

468468 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

470470 where pn ist = displaySpans .

471471 renderPretty 0.9 1000 .

472472 fmap (fancifyAnnots ist) .

473473 prettyName True True []

474474

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

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

476476 do ctxt <- getContext

477477 ist <- getIState

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

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

482482 []

483483 (idris_infixes ist)

484484 (delab ist tm'))

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

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

486486 displaySpans .

487487 renderPretty 0.9 80 .

488488 fmap (fancifyAnnots ist) $ ptm)

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

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

491− ideSlaveForceTermImplicits h id bnd True tm

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

493− ideSlaveForceTermImplicits h id bnd False tm

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

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

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

491+ ideModeForceTermImplicits h id bnd True tm

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

493+ ideModeForceTermImplicits h id bnd False tm

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

495495 case splitName name of

496496 Left err -> iPrintError err

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

499499 do ist <- getIState

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

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

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

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

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

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

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

504504 do ist <- getIState

505505 let (out, spans) =

506506 displaySpans .

507507 renderPretty 0.9 80 .

508508 fmap (fancifyAnnots ist) $ pprintErr ist e

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

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

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

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

511511

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

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

514−ideSlaveForceTermImplicits h id bnd impl tm =

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

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

514+ideModeForceTermImplicits h id bnd impl tm =

515515 do ist <- getIState

516516 let expl = annotate (AnnTerm bnd tm)

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

518518 bnd [] (idris_infixes ist)

519519 (delab ist tm))

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

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

521521 displaySpans .

522522 renderPretty 0.9 80 .

523523 fmap (fancifyAnnots ist) $ expl)

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

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

525525

526526splitName :: String -> Either String Name

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

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

11011101 case idris_outputmode ist of

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

11031103 return ()

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

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

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

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

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

11071107 where fc = fileFC "main"

11081108process fn (Compile codegen f)

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

14871487 do let inputs = opt getFile opts

14881488 let quiet = Quiet `elem` opts

14891489 let nobanner = NoBanner `elem` opts

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

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

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

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

14931493 let output = opt getOutput opts

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

16121612-- clearOrigPats

16131613 startServer port orig mods

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

1615− let idesock = IdeslaveSocket `elem` opts

1615+ let idesock = IdemodeSocket `elem` opts

16161616 when (idesl) $ ideslaveStart idesock orig inputs

16171617 ok <- noErrors

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

src/Idris/TypeSearch.hs+1−1

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

5757 case idris_outputmode i of

5858 RawOutput _ -> do mapM_ iRenderOutput docs

5959 iPrintResult ""

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

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

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

6262 where

6363 numLimit = 50