summary for ML modules made correct

This summary entry is special because its unfreeze may load ML
code that in turns adds summary entries.  Hence it is the first
summary piece to be unfreezed, otherwise some summaries may get
lost.

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

3 files changed, 19 insertions, 3 deletions

diff --git a/library/summary.ml b/library/summary.ml
index b46ce85b1..d1bbf7191 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -59,11 +59,22 @@ let freeze_summaries ~marshallable =
     summaries;
   !m
 
+let ml_modules = "ML-MODULES"
+let ml_modules_summary = mangle ml_modules
+
 let unfreeze_summaries fs =
+  (* The unfreezing of [ml_modules_summary] has to be anticipated since it
+   * may modify the content of [summaries] ny loading new ML modules *)
+  (try
+    (Hashtbl.find summaries ml_modules_summary).unfreeze_function 
+      (String.Map.find ml_modules_summary fs)
+  with Not_found -> anomaly (str"Undeclared summary "++str ml_modules_summary));
   Hashtbl.iter
     (fun id decl ->
-       try decl.unfreeze_function (String.Map.find id fs)
-       with Not_found -> decl.init_function())
+       if id = ml_modules_summary then () (* already unfreezed *)
+       else
+         try decl.unfreeze_function (String.Map.find id fs)
+         with Not_found -> decl.init_function())
     summaries
 
 let init_summaries () =
diff --git a/library/summary.mli b/library/summary.mli
index 38d5fc7e8..f6a9c6951 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -42,6 +42,11 @@ val declare_summary : string -> 'a summary_declaration -> unit
 
 val ref : ?freeze:(marshallable -> 'a -> 'a) -> name:string -> 'a -> 'a ref
 
+(** Special name for the summary of ML modules.  This summary entry is
+    special because its unfreeze may load ML code and hence add summary
+    entries.  Thus is has to be recognizable, and handled appropriately *)
+val ml_modules : string
+
 (** For global tables registered statically before the end of coqtop
     launch, the following empty [init_function] could be used. *)
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index ca4a5f648..09b604d1a 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -318,7 +318,7 @@ let unfreeze_ml_modules x =
   List.iter (cache_ml_object false false) x
 
 let _ =
-  Summary.declare_summary "ML-MODULES"
+  Summary.declare_summary Summary.ml_modules
     { Summary.freeze_function = (fun _ -> get_loaded_modules ());
       Summary.unfreeze_function = unfreeze_ml_modules;
       Summary.init_function = reset_loaded_modules }