diff options
| -rw-r--r-- | checker/check.ml | 29 | ||||
| -rw-r--r-- | checker/checker.ml | 17 | ||||
| -rw-r--r-- | kernel/names.ml | 2 | ||||
| -rw-r--r-- | kernel/names.mli | 7 | ||||
| -rw-r--r-- | library/library.ml | 34 |
5 files changed, 41 insertions, 48 deletions
diff --git a/checker/check.ml b/checker/check.ml index c3f0e976f..88306e214 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -234,28 +234,29 @@ let locate_qualified_library qid = (dir, file) with Not_found -> raise LibNotFound -let explain_locate_library_error qid = function - | LibUnmappedDir -> - let prefix = qid.dirpath in - errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) - | LibNotFound -> - errorlabstrm "load_absolute_library_from" - (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") - | e -> raise e +let error_unmapped_dir qid = + let prefix = qid.dirpath in + errorlabstrm "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 = + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") let try_locate_absolute_library dir = try locate_absolute_library dir - with e -> - explain_locate_library_error (path_of_dirpath dir) e + with + | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) + | LibNotFound -> error_lib_not_found (path_of_dirpath dir) let try_locate_qualified_library qid = try locate_qualified_library qid - with e -> - explain_locate_library_error qid e + with + | LibUnmappedDir -> error_unmapped_dir qid + | LibNotFound -> error_lib_not_found qid (************************************************************************) (*s Low-level interning/externing of libraries to files *) diff --git a/checker/checker.ml b/checker/checker.ml index 9834b1331..10a3089ed 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -70,8 +70,9 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d - with _ -> - if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + with Errors.UserError _ -> + if_verbose msg_warning + (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -279,9 +280,9 @@ let rec explain_exn = function report ()) | e when is_anomaly e -> print_anomaly e - | reraise -> + | e -> hov 0 (anomaly_string () ++ str "Uncaught exception " ++ - str (Printexc.to_string reraise)++report()) + str (Printexc.to_string e)++report()) let parse_args argv = let rec parse = function @@ -334,13 +335,7 @@ let parse_args argv = fatal_error (str "Unknown option " ++ str s) | s :: rem -> add_compile s; parse rem in - try - parse (List.tl (Array.to_list argv)) - with - | UserError(_, s) as e -> - if Pp.is_empty s then exit 1 - else fatal_error (explain_exn e) - | e -> begin fatal_error (explain_exn e) end + parse (List.tl (Array.to_list argv)) (* To prevent from doing the initialization twice *) diff --git a/kernel/names.ml b/kernel/names.ml index 976415e37..18f2ef0de 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,7 +34,7 @@ struct let check_soft x = let iter (fatal, x) = - if fatal then error x else Pp.msg_warning (str x) + if fatal then Errors.error x else Pp.msg_warning (str x) in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/names.mli b/kernel/names.mli index 77d5ce8e6..96a7dff09 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -20,15 +20,16 @@ sig (** Comparison over identifiers *) val check : string -> unit - (** Check that a string may be converted to an identifier. Raise an exception - related to the problem when this is not the case. *) + (** Check that a string may be converted to an identifier. + Raise a [UserError _] exception related to the problem + when this is not the case. *) val check_soft : string -> unit (** As [check], but may raise a warning instead of failing when the string is not an identifier, but is a well-formed string. *) val of_string : string -> t - (** Converts a string into an identifier. *) + (** Converts a string into an identifier. May raise [UserError _] *) val to_string : t -> string (** Converts a identifier into an string. *) diff --git a/library/library.ml b/library/library.ml index 9938333f2..0243968b9 100644 --- a/library/library.ml +++ b/library/library.ml @@ -358,34 +358,30 @@ let locate_qualified_library warn qid = else (LibInPath, dir, file) with Not_found -> raise LibNotFound -let explain_locate_library_error qid = function - | LibUnmappedDir -> - let prefix, _ = repr_qualid qid in - errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) - | LibNotFound -> - errorlabstrm "load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - | e -> - let e = Errors.push e in - raise e +let error_unmapped_dir qid = + let prefix, _ = repr_qualid qid in + errorlabstrm "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 = + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") let try_locate_absolute_library dir = try locate_absolute_library dir - with e -> - let e = Errors.push e in - explain_locate_library_error (qualid_of_dirpath dir) e + with + | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) + | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) let try_locate_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f - with e -> - let e = Errors.push e in - explain_locate_library_error qid e - + with + | LibUnmappedDir -> error_unmapped_dir qid + | LibNotFound -> error_lib_not_found qid (************************************************************************) (* Internalise libraries *) |