@@ -109,6 +109,10 @@ ideslave orig mods
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') -> idrisCatch
113+ (do process fn (Prove n')
114+ isetPrompt (mkPrompt mods))
115+ (\e -> do iFail $ show e)
112 Right cmd -> idrisCatch
116 Right cmd -> idrisCatch
113 (do ideslaveProcess fn cmd)
117 (do ideslaveProcess fn cmd)
114 (\e -> do iFail $ show e)
118 (\e -> do iFail $ show e)
@@ -149,7 +153,6 @@ ideslaveProcess fn (Search t) = process fn (Search t)
149ideslaveProcess fn (Spec t) = process fn (Spec t)
153ideslaveProcess fn (Spec t) = process fn (Spec t)
150-- RmProof and AddProof not supported!
154-- RmProof and AddProof not supported!
151ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
155ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
152−ideslaveProcess fn (Prove n') = process fn (Prove n')
153ideslaveProcess fn (HNF t) = process fn (HNF t)
156ideslaveProcess fn (HNF t) = process fn (HNF t)
154--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
157--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!