From 80aba8d52c650ef8e4ada694c20bf12c15849694 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 8 Aug 2013 18:52:47 +0000
Subject: 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
---
 library/lib.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'library/lib.ml')

diff --git a/library/lib.ml b/library/lib.ml
index b4371812b2..379d0e8ad0 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -250,7 +250,7 @@ let add_anonymous_leaf obj =
 
 let add_frozen_state () =
   add_anonymous_entry
-    (FrozenState (Summary.freeze_summaries ~marshallable:false))
+    (FrozenState (Summary.freeze_summaries ~marshallable:`No))
 
 (* Modules. *)
 
@@ -485,7 +485,7 @@ let open_section id =
   let name = make_path id, make_kn id (* this makes little sense however *) in
   if Nametab.exists_section dir then
     errorlabstrm "open_section" (pr_id id ++ str " already exists.");
-  let fs = Summary.freeze_summaries ~marshallable:false in
+  let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry name (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
@@ -529,7 +529,9 @@ let close_section () =
 
 type frozen = Names.DirPath.t option * library_segment
 
-let freeze ~marshallable:_ = (!comp_name, !lib_stk)
+let freeze ~marshallable =
+  if marshallable = `Shallow then !comp_name, []
+  else !comp_name, !lib_stk
 
 let unfreeze (mn,stk) =
   comp_name := mn;
-- 
cgit v1.2.3