diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:35:47 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:46:38 +0200 |
commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /checker | |
parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff) |
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'checker')
-rw-r--r-- | checker/check.ml | 12 | ||||
-rw-r--r-- | checker/checker.ml | 4 | ||||
-rw-r--r-- | checker/modops.ml | 2 | ||||
-rw-r--r-- | checker/safe_typing.ml | 2 |
4 files changed, 11 insertions, 9 deletions
diff --git a/checker/check.ml b/checker/check.ml index 38d2057eb..8565e96fc 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -247,12 +247,12 @@ let locate_qualified_library qid = let error_unmapped_dir qid = let prefix = qid.dirpath in - user_err "load_absolute_library_from" + user_err ~hdr:"load_absolute_library_from" (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirlist 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_path qid ++ str" in loadpath") let try_locate_absolute_library dir = @@ -313,18 +313,18 @@ let intern_from_file (dir, f) = let () = close_in ch in let ch = open_in_bin f in if not (String.equal (Digest.channel ch pos) checksum) then - user_err "intern_from_file" (str "Checksum mismatch"); + user_err ~hdr:"intern_from_file" (str "Checksum mismatch"); let () = close_in ch in if dir <> sd.md_name then - user_err "intern_from_file" + user_err ~hdr:"intern_from_file" (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then - user_err "intern_from_file" + user_err ~hdr:"intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin Feedback.msg_notice(str " (was a vio file) "); Option.iter (fun (_,_,b) -> if not b then - user_err "intern_from_file" + user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; Validate.validate !Flags.debug Values.v_univopaques opaque_csts; diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44..06d0cd1c0 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -213,7 +213,9 @@ let report () = (str "." ++ spc () ++ str "Please report.") let guill s = str "\"" ++ str s ++ str "\"" -let where s = +let where = function +| None -> mt () +| Some s -> if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) let rec explain_exn = function diff --git a/checker/modops.ml b/checker/modops.ml index de1db6e35..aba9da2fe 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -33,7 +33,7 @@ let error_no_such_label_sub l l1 = Label.to_string l^" is missing in "^l1^".") let error_not_a_module_loc loc s = - user_err ~loc "" (str ("\""^Label.to_string s^"\" is not a module")) + user_err ~loc (str ("\""^Label.to_string s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc Loc.ghost s diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index c0b3a3e73..f7cd4d6f6 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -89,6 +89,6 @@ let import file clib univs digest = let unsafe_import file clib univs digest = let env = !genv in if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps - else check_imports (user_err"unsafe_import") clib.comp_name env clib.comp_deps; + else check_imports (user_err (str "unsafe_import")) clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest |