git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1006 from david-christiansen/ideslave-opts

Allow getting and setting options from IDESlave

commitdfb3982e3d929e140d922ea2b548271f6432700d authorEdwin Brady <edwin.brady@gmail.com> dateWed 26 Mar 2014, 20:03 (13 years ago) parent89c89d38325ced
3 files changed+27−2
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/IdeSlave.hs+9−1 src/Idris/REPL.hs+17
src/Idris/AbsSyntax.hs+1−1
@@ -10,7 +10,7 @@ import Idris.Core.Typecheck
1010import Idris.AbsSyntaxTree
1111import Idris.Colours
1212import Idris.Docstrings
13−import Idris.IdeSlave
13+import Idris.IdeSlave hiding (Opt(..))
1414import IRTS.CodegenCommon
1515import Util.DynamicLinker
1616
src/Idris/IdeSlave.hs+9−1
@@ -1,6 +1,6 @@
11{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}
22
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
44
55import Text.Printf
66import Numeric
@@ -130,6 +130,8 @@ quotedChar = try (string "\\\\" >> return '\\')
130130parseSExp :: String -> Result SExp
131131parseSExp = parseString pSExp (Directed (UTF8.fromString "(unknown)") 0 0 0 0)
132132
133+data Opt = ShowImpl | ErrContext deriving Show
134+
133135data IdeSlaveCommand = REPLCompletions String
134136 | Interpret String
135137 | TypeOf String
@@ -142,6 +144,8 @@ data IdeSlaveCommand = REPLCompletions String
142144 | LoadFile String
143145 | DocsFor String
144146 | Apropos String
147+ | GetOpts
148+ | SetOpt Opt Bool
145149 deriving Show
146150
147151sexpToCommand :: SExp -> Maybe IdeSlaveCommand
@@ -161,6 +165,10 @@ sexpToCommand (SexpList [SymbolAtom "proof-search", IntegerAtom line, StringAtom
161165 _ -> Nothing)
162166sexpToCommand (SexpList [SymbolAtom "docs-for", StringAtom name]) = Just (DocsFor name)
163167sexpToCommand (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
164172sexpToCommand _ = Nothing
165173
166174parseMessage :: String -> Either Err (SExp, Integer)
src/Idris/REPL.hs+17
@@ -268,6 +268,23 @@ ideslave orig mods
268268 process stdout fn (DoProofSearch False line (sUN name) (map sUN hints))
269269 Just (IdeSlave.Apropos a) ->
270270 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
271288 Nothing -> do iPrintError "did not understand")
272289 (\e -> do iPrintError $ show e))
273290 (\e -> do iPrintError $ show e)