From 622806fb27fb0752cdbd2b252da1caa0513b585b Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sat, 5 Aug 2017 18:21:10 +0100 Subject: Print names of all open blocks Fixes bug 5597. --- library/lib.ml | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index a24d20c68..dc903df09 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -162,6 +162,13 @@ let find_entry_p p = in find !lib_state.lib_stk +let find_entries_p p = + let rec find = function + | [] -> [] + | ent::l -> if p ent then ent::find l else find l + in + find !lib_state.lib_stk + let split_lib_gen test = let rec collect after equal = function | hd::before when test hd -> collect after (hd::equal) before @@ -328,16 +335,18 @@ let start_compilation s mp = lib_state := { !lib_state with comp_name = Some s; path_prefix = prefix } +let open_blocks_message es = + let open_block_name = function + | oname, OpenedSection _ -> str "section " ++ pr_id (basename (fst oname)) + | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ pr_id (basename (fst oname)) + | _ -> assert false in + str "The " ++ pr_enum open_block_name es ++ spc () ++ + str "need" ++ str (if List.length es == 1 then "s" else "") ++ str " to be closed." + let end_compilation_checks dir = - let _ = - try match snd (find_entry_p is_opening_node) with - | OpenedSection _ -> user_err Pp.(str "There are some open sections.") - | OpenedModule (ty,_,_,_) -> - user_err ~hdr:"Lib.end_compilation_checks" - (str "There are some open " ++ str (module_kind ty) ++ str "s.") - | _ -> assert false - with Not_found -> () - in + let _ = match find_entries_p is_opening_node with + | [] -> () + | es -> user_err ~hdr:"Lib.end_compilation_checks" (open_blocks_message es) in let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false in let oname = -- cgit v1.2.3