enhance marshallable option for freeze (minor TODO in safe_typing)

It can be:
`Yes      Full data, in a state that can be marshalled
`No       Full data, good for Undo only
`Shallow  Partial data, marshallable, good for slave processes

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

4 files changed, 15 insertions, 8 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1dba380016..394cce6ced 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -128,7 +128,7 @@ let compile_files () =
     | [] -> ()
     | [vf] -> compile_file vf (* One compilation : no need to save init state *)
     | l ->
-      let init_state = States.freeze ~marshallable:false in
+      let init_state = States.freeze ~marshallable:`No in
       let coqdoc_init_state = Lexer.location_table () in
       List.iter
         (fun vf ->
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 46037bcbc5..e9fd0620d0 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1075,7 +1075,7 @@ let inNotation : notation_obj -> obj =
 (**********************************************************************)
 
 let with_lib_stk_protection f x =
-  let fs = Lib.freeze false in
+  let fs = Lib.freeze `No in
   try let a = f x in Lib.unfreeze fs; a
   with reraise ->
     let reraise = Errors.push reraise in
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 218929f233..d9d63d7969 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -382,7 +382,7 @@ end = struct (* {{{ *)
   (* hack to make futures functional *)
   let in_t, out_t = Dyn.create "state4future"
   let () = Future.set_freeze
-    (fun () -> in_t (freeze_global_state (), !cur_id))
+    (fun () -> in_t (freeze_global_state `No, !cur_id))
     (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
 
   let is_cached id =
@@ -407,14 +407,21 @@ end = struct (* {{{ *)
     Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
     Stateid.add_state_id e ?valid id
 
-  let define ?(cache=false) f id =
+  let string_of_cache = function
+    | `Yes -> "Yes" | `No -> "No" | `Marshallable -> "Marshallable"
+  let marshallable_of_cache = function
+    | `Yes -> `No
+    | `No -> assert false
+    | `Marshallable -> `Shallow
+
+  let define ?(cache=`No) f id =
     if is_cached id then
       anomaly (str"defining state "++str(string_of_state_id id)++str" twice");
     try
       prerr_endline ("defining " ^
         string_of_state_id id ^ " (cache=" ^ string_of_bool cache ^ ")");
       f ();
-      if cache then freeze id;
+      if cache <> `No then freeze (marshallable_of_cache cache) id;
       cur_id := id;
       feedback ~state_id:id Interface.Processed;
       VCS.reached id true;
@@ -466,8 +473,8 @@ let known_state ~cache id =
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
    * side effects *)
   let cherry_pick_non_pstate () =
-    Summary.freeze_summary ~marshallable:false ~complement:true pstate,
-    Lib.freeze ~marshallable:false in
+    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
+    Lib.freeze ~marshallable:`No in
   let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
 
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 88802fc34e..888c3411d8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -188,7 +188,7 @@ let set_formatter_translator() =
 let pr_new_syntax loc ocom =
   let loc = Loc.unloc loc in
   if !beautify_file then set_formatter_translator();
-  let fs = States.freeze ~marshallable:false in
+  let fs = States.freeze ~marshallable:`No in
   let com = match ocom with
     | Some VernacNop -> mt()
     | Some com -> Ppvernac.pr_vernac com