aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-03-06 20:23:52 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-03-07 17:31:47 +0000
commit5cbb460234e32f5e325c60aaada91d3cea298b9f (patch)
treeacbdf6d7f5282db34d1866371cf156c7f51759e2 /library
parent33bf4f2c5c60114eb6db4a8e082ff8882923f6c8 (diff)
Use a proper warning when a summary is captured out of module scope.
Diffstat (limited to 'library')
-rw-r--r--library/summary.ml12
1 files changed, 11 insertions, 1 deletions
diff --git a/library/summary.ml b/library/summary.ml
index 6ca871555..7ef19fbfb 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -89,6 +89,16 @@ let unfreeze_single name state =
Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]);
iraise e
+let warn_summary_out_of_scope =
+ let name = "summary-out-of-scope" in
+ let category = "dev" in
+ let default = CWarnings.Disabled in
+ CWarnings.create ~name ~category ~default (fun name ->
+ Pp.str (Printf.sprintf
+ "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s"
+ name)
+ )
+
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 *)
@@ -101,7 +111,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } =
try decl.unfreeze_function String.Map.(find name summaries)
with Not_found ->
if not partial then begin
- Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name);
+ warn_summary_out_of_scope name;
decl.init_function ()
end;
in