Imported Upstream version 8.5~beta1+dfsg

1 files changed, 18 insertions, 18 deletions

diff --git a/library/states.ml b/library/states.ml
index 768fbb23..a1c2a095 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -1,46 +1,46 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
 open System
 
 type state = Lib.frozen * Summary.frozen
 
-let freeze () =
-  (Lib.freeze(), Summary.freeze_summaries())
+let summary_of_state = snd
+
+let freeze ~marshallable =
+  (Lib.freeze ~marshallable, Summary.freeze_summaries ~marshallable)
 
 let unfreeze (fl,fs) =
   Lib.unfreeze fl;
   Summary.unfreeze_summaries fs
 
 let (extern_state,intern_state) =
+  let ensure_suffix f = CUnix.make_suffix f ".coq" in
   let (raw_extern, raw_intern) =
-    extern_intern Coq_config.state_magic_number ".coq" in
+    extern_intern Coq_config.state_magic_number in
   (fun s ->
-    if !Flags.load_proofs <> Flags.Force then
-      Util.error "Write State only works with option -force-load-proofs";
-    raw_extern s (freeze())),
+    let s = ensure_suffix s in
+    raw_extern s (freeze ~marshallable:`Yes)),
   (fun s ->
-    unfreeze
-      (with_magic_number_check (raw_intern (Library.get_load_paths ())) s);
+    let s = ensure_suffix s in
+    let paths = Loadpath.get_paths () in
+    unfreeze (with_magic_number_check (raw_intern paths) s);
     Library.overwrite_library_filenames s)
 
 (* Rollback. *)
 
-let with_heavy_rollback f h x =
-  let st = freeze () in
-  try
-    f x
-  with reraise ->
-    let e = h reraise in (unfreeze st; raise e)
-
 let with_state_protection f x =
-  let st = freeze () in
+  let st = freeze ~marshallable:`No in
   try
     let a = f x in unfreeze st; a
   with reraise ->
-    (unfreeze st; raise reraise)
+    let reraise = Errors.push reraise in
+    (unfreeze st; iraise reraise)
+
+let with_state_protection_on_exception = Future.transactify