From 5676b113920fb48d4898817d6c0ce3353b06107f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 29 Nov 2017 01:42:21 +0100 Subject: [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. --- library/summary.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'library/summary.ml') 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 -- cgit v1.2.3