diff options
| -rw-r--r-- | library/summary.ml | 15 | ||||
| -rw-r--r-- | library/summary.mli | 5 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 2 |
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 } |