diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 01:42:21 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-09 18:17:50 +0100 |
| commit | 5676b113920fb48d4898817d6c0ce3353b06107f (patch) | |
| tree | 71dbe3f412ec441fd72dbf02a70ce9bb3e9a06c7 /library/summary.ml | |
| parent | 8c9166435d6926babf697c3f575a8653f465cc76 (diff) | |
[summary] Adapt STM to the new Summary API.
We need to a partial restore. I think that we could design a better
API, but further work on the toplevel state should improve it
progressively.
Diffstat (limited to 'library/summary.ml')
| -rw-r--r-- | library/summary.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/library/summary.ml b/library/summary.ml index 5fe3160e1..6df17476b 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -87,7 +87,7 @@ let unfreeze_single name state = Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); iraise e -let unfreeze_summaries { summaries; ml_module } = +let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it * may modify the content of [summaries] by loading new ML modules *) begin match !sum_mod with @@ -98,8 +98,10 @@ let unfreeze_summaries { summaries; ml_module } = let ufz name decl = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> - Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); - decl.init_function () + if not partial then begin + Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + decl.init_function () + end; in (* String.Map.iter unfreeze_single !sum_map *) String.Map.iter ufz !sum_map |