From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- library/library.ml | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'library/library.ml') diff --git a/library/library.ml b/library/library.ml index 8d3916a97..c3d0485d3 100644 --- a/library/library.ml +++ b/library/library.ml @@ -131,7 +131,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - user_err "Library.find_library" + user_err ~hdr:"Library.find_library" (str "Unknown library " ++ pr_dirpath dir) let register_library_filename dir f = @@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid = let error_unmapped_dir qid = let prefix, _ = repr_qualid qid in - user_err "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) let error_lib_not_found qid = - user_err "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -378,7 +378,7 @@ let access_table what tables dp i = let t = try fetch_delayed f with Faulty f -> - user_err "Library.access_table" + user_err ~hdr:"Library.access_table" (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++ str ") is inaccessible or corrupted,\ncannot load some " ++ str what ++ str " in it.\n") @@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from = let f = match f with Some f -> f | None -> try_locate_absolute_library dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then - user_err "load_physical_library" + user_err ~hdr:"load_physical_library" (str "The file " ++ str f ++ str " contains library" ++ spc () ++ pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); @@ -477,7 +477,7 @@ and intern_library_deps libs dir m from = and intern_mandatory_library caller from libs (dir,d) = let digest, libs = intern_library libs (dir, None) from in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - user_err "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); + user_err (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = @@ -572,7 +572,7 @@ let require_library_from_dirpath modrefl export = let safe_locate_module (loc,qid) = try Nametab.locate_module qid with Not_found -> - user_err ~loc "import_library" + user_err ~loc ~hdr:"import_library" (pr_qualid qid ++ str " is not a module") let import_module export modl = @@ -597,7 +597,7 @@ let import_module export modl = flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err ~loc "import_library" + user_err ~loc ~hdr:"import_library" (pr_qualid dir ++ str " is not a module")) | [] -> flush acc in aux [] modl @@ -609,7 +609,7 @@ let check_coq_overwriting p id = let l = DirPath.repr p in let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then - user_err "" + user_err (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") @@ -622,7 +622,7 @@ let check_module_name s = (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++ strbrk " is not allowed in module names\n" in - let err c = user_err "" (msg c) in + let err c = user_err (msg c) in match String.get s 0 with | 'a' .. 'z' | 'A' .. 'Z' -> for i = 1 to (String.length s)-1 do @@ -658,10 +658,10 @@ let load_library_todo f = let tasks, _, _ = System.marshal_in_segment f ch in let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; - if tasks = None then user_err "restart" (str"not a .vio file"); - if s2 = None then user_err "restart" (str"not a .vio file"); - if s3 = None then user_err "restart" (str"not a .vio file"); - if pi3 (Option.get s2) then user_err "restart" (str"not a .vio file"); + if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); + if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 (************************************************************************) @@ -677,7 +677,7 @@ let current_deps () = let current_reexports () = !libraries_exports_list let error_recursively_dependent_library dir = - user_err "" + user_err (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") @@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab = except Int.Set.empty in let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in Array.iteri (fun i x -> - if not(is_done_or_todo i x) then CErrors.user_err "library" + if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) opaque_table; let sd = { -- cgit v1.2.3