git.iko.soy/Idris-dev
on master help sign in
more work on the prove mode... now sending messages when it started and finished
1721a22Hannes Mehnert
src/Idris/IdeSlave.hs+10
compare with master
unifiedsplit
@@ -8,6 +8,8 @@ import Data.List
8-- import qualified Data.Text as T
8-- import qualified Data.Text as T
9import Text.Parsec
9import Text.Parsec
10
10
11+import Core.TT
12+
11data SExp = SexpList [SExp]
13data SExp = SexpList [SExp]
12 | StringAtom String
14 | StringAtom String
13 | BoolAtom Bool
15 | BoolAtom Bool
@@ -42,6 +44,14 @@ instance SExpable Integer where
42instance SExpable Int where
44instance SExpable Int where
43 toSExp n = IntegerAtom (toInteger n)
45 toSExp n = IntegerAtom (toInteger n)
44
46
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+
45instance (SExpable a) => SExpable (Maybe a) where
55instance (SExpable a) => SExpable (Maybe a) where
46 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
56 toSExp Nothing = SexpList [SymbolAtom "Nothing"]
47 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
57 toSExp (Just a) = SexpList [SymbolAtom "Just", toSExp a]
src/Idris/REPL.hs+9−4
@@ -109,10 +109,15 @@ ideslave orig mods
109 _ -> ""
109 _ -> ""
110 case parseCmd i cmd of
110 case parseCmd i cmd of
111 Left err -> iFail $ show err
111 Left err -> iFail $ show err
112+ Right (Prove n') -> do iResult ""
113+ liftIO $ putStrLn $ convSExp "proof-mode" (True, n') id
112− Right (Prove n') -> idrisCatch
114+ idrisCatch
113− (do process fn (Prove n')
115+ (do process fn (Prove n'))
114− isetPrompt (mkPrompt mods))
115− (\e -> do iFail $ show e)
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)
116 Right cmd -> idrisCatch
121 Right cmd -> idrisCatch
117 (do ideslaveProcess fn cmd)
122 (do ideslaveProcess fn cmd)
118 (\e -> do iFail $ show e)
123 (\e -> do iFail $ show e)