dfb3982 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1006 from david-christiansen/ideslave-opts

dfb3982Edwin Brady13 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

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

10import Idris.AbsSyntaxTree

11import Idris.Colours

12import Idris.Docstrings

13−import Idris.IdeSlave

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

14import IRTS.CodegenCommon

15import Util.DynamicLinker

src/Idris/IdeSlave.hs+9−1

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

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

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

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

5import Text.Printf

6import Numeric

@@ -130,6 +130,8 @@ quotedChar = try (string "\\\\" >> return '\\')

130parseSExp :: String -> Result SExp

131parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)

132

133+data Opt = ShowImpl | ErrContext deriving Show

134+

133data IdeSlaveCommand = REPLCompletions String

135data IdeSlaveCommand = REPLCompletions String

134 | Interpret String

136 | Interpret String

135 | TypeOf String

137 | TypeOf String

@@ -142,6 +144,8 @@ data IdeSlaveCommand = REPLCompletions String

142 | LoadFile String

144 | LoadFile String

143 | DocsFor String

145 | DocsFor String

144 | Apropos String

146 | Apropos String

147+ | GetOpts

148+ | SetOpt Opt Bool

145 deriving Show

149 deriving Show

146

150

147sexpToCommand :: SExp -> Maybe IdeSlaveCommand

151sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -161,6 +165,10 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom

161 _ -> Nothing)

165 _ -> Nothing)

162sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

166sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)

163sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

167sexpToCommand (SexpList [SymbolAtom "apropos", StringAtom search]) = Just (Apropos search)

168+sexpToCommand (SymbolAtom "get-options") = Just GetOpts

169+sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

170+ | Just opt <- lookup s opts = Just (SetOpt opt b)

171+ where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

164sexpToCommand _ = Nothing

172sexpToCommand _ = Nothing

165

173

166parseMessage :: String -> Either Err (SExp, Integer)

174parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+17

@@ -268,6 +268,23 @@ ideslave orig mods

268 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))

269 Just (IdeSlave.Apropos a) ->

270 process stdout fn (Apropos a)

271+ Just (IdeSlave.GetOpts) ->

272+ do ist <- getIState

273+ let opts = idris_options ist

274+ let impshow = opt_showimp opts

275+ let errCtxt = opt_errContext opts

276+ let options = (IdeSlave.SymbolAtom "ok",

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

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

279+ runIO . putStrLn $ IdeSlave.convSExp "return" options id

280+ Just (IdeSlave.SetOpt IdeSlave.ShowImpl b) ->

281+ do setImpShow b

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

283+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

284+ Just (IdeSlave.SetOpt IdeSlave.ErrContext b) ->

285+ do setErrContext b

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

287+ runIO . putStrLn $ IdeSlave.convSExp "return" msg id

271 Nothing -> do iPrintError "did not understand")

288 Nothing -> do iPrintError "did not understand")

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

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

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

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