From cccabf3859d3b7fb79d0a9f477ea284d38a70dab Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 27 Dec 2013 14:48:25 +0100
Subject: STM: fix error messages while in batch mode (closes: 3196)

---
 toplevel/stm.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 86b7794e8b..57bbafac3a 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1529,7 +1529,8 @@ let handle_failure e vcs tty =
   | None ->
       VCS.restore vcs;
       VCS.print ();
-      if tty then begin (* Hopefully the 1 to last state is valid *)
+      if tty && interactive () = `Yes then begin
+        (* Hopefully the 1 to last state is valid *)
         Backtrack.back_safe (); 
         VCS.checkout_shallowest_proof_branch ();
       end;
@@ -1539,7 +1540,8 @@ let handle_failure e vcs tty =
   | Some (safe_id, id) ->
       prerr_endline ("Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
-      if tty then begin (* We stay on a valid state *)
+      if tty && interactive () = `Yes then begin
+        (* We stay on a valid state *)
         Backtrack.backto safe_id;
         VCS.checkout_shallowest_proof_branch ();
         Reach.known_state ~cache:(interactive ()) safe_id;
@@ -1847,7 +1849,9 @@ let interp verb (_,e as lexpr) =
   let clas = classify_vernac e in
   let rc = process_transaction ~tty:true verb clas lexpr in
   if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
-  if interactive () = `Yes then
+  if interactive () = `Yes ||
+     (!Flags.async_proofs_mode = Flags.APoff &&
+      !Flags.compilation_mode = Flags.BuildVo) then
     let vcs = VCS.backup () in
     try finish ()
     with e ->
-- 
cgit v1.2.3