coqtop -compile: avoid with_heavy_rollback when non-interactive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 20 insertions, 7 deletions

diff --git a/library/states.ml b/library/states.ml
index eb597670f..8b8193981 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -39,6 +39,10 @@ let with_heavy_rollback f h x =
   with reraise ->
     let e = h reraise in (unfreeze st; raise e)
 
+let without_rollback f h x =
+  try f x
+  with reraise -> raise (h reraise)
+
 let with_state_protection f x =
   let st = freeze () in
   try
diff --git a/library/states.mli b/library/states.mli
index 7e6535d92..26dec09e5 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -22,14 +22,20 @@ val unfreeze : state -> unit
 
 (** {6 Rollback } *)
 
-(** [with_heavy_rollback f x] applies [f] to [x] and restores the
-  state of the whole system as it was before the evaluation if an exception
-  is raised. *)
+(** [with_heavy_rollback f h x] applies [f] to [x]. If this application
+    ends on an exception, the wrapper [h] is applied to it, then
+    the state of the whole system is restored as it was before applying [f],
+    and finally the exception produced by [h] is raised. *)
+
 val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
 
+(** [without_rollback] is just like [with_heavy_rollback], except that
+    no state is restored in case of exception. *)
+
+val without_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
+
 (** [with_state_protection f x] applies [f] to [x] and restores the
-  state of the whole system as it was before the evaluation of f *)
+  state of the whole system as it was before applying [f] *)
 
 val with_state_protection : ('a -> 'b) -> 'a -> 'b
 
-
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e037944f2..67befcb17 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -321,11 +321,14 @@ let rec vernac_com interpfun checknav (loc,com) =
 	  interp v
 
     | v ->
+          let rollback =
+            if !Flags.batch_mode then States.without_rollback
+            else States.with_heavy_rollback
+          in
 	  let psh = default_set_timeout () in
 	  try
             let status =
-              States.with_heavy_rollback interpfun
-                Cerrors.process_vernac_interp_error v
+              rollback interpfun Cerrors.process_vernac_interp_error v
             in
 	    restore_timeout psh;
             status