git.iko.soy/Idris-dev
on master help sign in
more work on the prove mode... now sending messages when it started and finished
commit1721a22e8be10b034f69a3a4a4b0d364489635b2 authorHannes Mehnert <hannes@mehnert.org> dateSat 18 May 2013, 20:35 (13 years ago) parent5242001
2 files changed+19−4
compare with master
unifiedsplit
src/Idris/IdeSlave.hs+10 src/Idris/REPL.hs+9−4
src/Idris/IdeSlave.hs+10
@@ -8,6 +8,8 @@ import Data.List
88-- import qualified Data.Text as T
99import Text.Parsec
1010
11+import Core.TT
12+
1113data SExp = SexpList [SExp]
1214 | StringAtom String
1315 | BoolAtom Bool
@@ -42,6 +44,14 @@ instance SExpable Integer where
4244instance SExpable Int where
4345 toSExp n = IntegerAtom (toInteger n)
4446
47+
48+instance SExpable Name where
49+ toSExp (UN s) = SexpList [SymbolAtom "UN", StringAtom s]
50+ toSExp (NS s ns) = SexpList [SymbolAtom "NS", toSExp s, toSExp ns]
51+ toSExp (MN n s) = SexpList [SymbolAtom "MN", toSExp n, toSExp s]
52+ toSExp NErased = SexpList [SymbolAtom "NErased"]
53+
54+
4555instance (SExpable a) => SExpable (Maybe a) where
4656 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
4757 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
src/Idris/REPL.hs+9−4
@@ -109,10 +109,15 @@ ideslave orig mods
109109 _ -> ""
110110 case parseCmd i cmd of
111111 Left err -> iFail $ show err
112− Right (Prove n') -> idrisCatch
113− (do process fn (Prove n')
114− isetPrompt (mkPrompt mods))
115− (\e -> do iFail $ show e)
112+ Right (Prove n') -> do iResult ""
113+ liftIO $ putStrLn $ convSExp "proof-mode" (True, n') id
114+ idrisCatch
115+ (do process fn (Prove n'))
116+ (\e -> do iFail $ show e)
117+ i <- getIState
118+ case (idris_outputmode i) of
119+ IdeSlave id -> liftIO $ putStrLn $ convSExp "proof-mode" (False, n') id
120+ isetPrompt (mkPrompt mods)
116121 Right cmd -> idrisCatch
117122 (do ideslaveProcess fn cmd)
118123 (\e -> do iFail $ show e)