From 60b1e4b4cc6783013e055838f5f2f5cca10f7d75 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 29 Sep 1999 07:34:20 +0000
Subject: with_heavy_rollback deplace dans States

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@89 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml     | 13 -------------
 library/lib.mli    |  7 -------
 library/states.ml  | 13 +++++++++++++
 library/states.mli |  9 +++++++++
 toplevel/vernac.ml |  4 ++--
 5 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/library/lib.ml b/library/lib.ml
index 470c85674..07d4049ce 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -186,16 +186,3 @@ let init () =
   add_frozen_state ();
   path_prefix := []
 
-
-(* Rollback. *)
-
-let with_heavy_rollback f x =
-  let sum = freeze_summaries ()
-  and flib = freeze() in
-  try 
-    f x
-  with reraise -> begin
-    unfreeze_summaries sum;
-    unfreeze flib;
-    raise reraise
-  end
diff --git a/library/lib.mli b/library/lib.mli
index 33f6e9056..d8b3def29 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -48,13 +48,6 @@ val export_module : unit -> library_segment
 val reset_to : section_path -> unit
 
 
-(*s 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. *)
-
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
-
-
 (*s We can get and set the state of the operations (used in [States]). *)
 
 type frozen
diff --git a/library/states.ml b/library/states.ml
index 2e198e36f..d8fed1437 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -20,3 +20,16 @@ let (extern_state,intern_state) =
   let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in
   (fun s -> raw_extern s (get_state())),
   (fun s -> set_state (raw_intern s))
+
+(* Rollback. *)
+
+let with_heavy_rollback f x =
+  let sum = freeze_summaries ()
+  and flib = freeze() in
+  try 
+    f x
+  with reraise -> begin
+    unfreeze_summaries sum;
+    unfreeze flib;
+    raise reraise
+  end
diff --git a/library/states.mli b/library/states.mli
index 06a877802..d648a68ce 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,8 +1,17 @@
 
 (* $Id$ *)
 
+(*s States of the system. *)
+
 type state
 
 val intern_state : string -> unit
 val extern_state : string -> unit
 
+(*s 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. *)
+
+val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+
+
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index d0a0c63ff..65bb4f4d8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -100,7 +100,7 @@ let rec vernac interpfun input =
                                Str (_,mname); Str(_,fname)]) ->
           let verbosely = verbosely = "Verbose" in
           let only_spec = only_spec = "Specification" in
-          Lib.with_heavy_rollback (* to roll back in case of error *)
+          States.with_heavy_rollback (* to roll back in case of error *)
             (raw_compile_module verbosely only_spec mname)
             (make_suffix fname ".v")
       | _ -> if not !just_parsing then interpfun com
@@ -144,7 +144,7 @@ and read_vernac_file verbosely s =
  * parses and executes one command of the vernacular char stream *)
 
 let raw_do_vernac po =
-  vernac (Lib.with_heavy_rollback Vernacinterp.interp) (po,None)
+  vernac (States.with_heavy_rollback Vernacinterp.interp) (po,None)
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
-- 
cgit v1.2.3