@@ -109,6 +109,10 @@ 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)
112116 Right cmd -> idrisCatch
113117 (do ideslaveProcess fn cmd)
114118 (\e -> do iFail $ show e)
@@ -149,7 +153,6 @@ ideslaveProcess fn (Search t) = process fn (Search t)
149153ideslaveProcess fn (Spec t) = process fn (Spec t)
150154-- RmProof and AddProof not supported!
151155ideslaveProcess fn (ShowProof n') = process fn (ShowProof n')
152−ideslaveProcess fn (Prove n') = process fn (Prove n')
153156ideslaveProcess fn (HNF t) = process fn (HNF t)
154157--ideslaveProcess fn TTShell = process fn TTShell -- need some prove mode!
155158