diff options
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/lib.mli | 1 | ||||
| -rw-r--r-- | library/library.ml | 2 |
3 files changed, 7 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index c46a3833bf..9438713d6c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -139,6 +139,10 @@ let start_module s = let is_opened_section = function (_,OpenedSection _) -> true | _ -> false +let sections_are_opened () = + try let _ = find_entry_p is_opened_section in true + with Not_found -> false + let export_segment seg = let rec clean acc = function | (_,Module _) :: _ | [] -> acc diff --git a/library/lib.mli b/library/lib.mli index f8a126cce5..9b5326db1e 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -50,6 +50,7 @@ val contents_after : section_path option -> library_segment val open_section : string -> section_path val close_section : export:bool -> string -> section_path * library_segment * Summary.frozen +val sections_are_opened : unit -> bool val make_path : identifier -> path_kind -> section_path val cwd : unit -> dir_path diff --git a/library/library.ml b/library/library.ml index 48af3672af..bea05a2229 100644 --- a/library/library.ml +++ b/library/library.ml @@ -200,6 +200,8 @@ let (in_require, _) = export_function = (fun _ -> None) }) let require_module spec name fileopt export = + if sections_are_opened () then + warning ("Objets of "^name^" not surviving sections (e.g. Grammar \nand Hints) will be removed at the end of the section"); let file = match fileopt with | None -> name | Some f -> f |