Restrict (try...with...) to avoid catching critical exn (part 1)

 Why? : avoid catching (and probably ignoring) exceptions
 such as Sys.Break, anomalies, assertions, leading to undetected
 bugs and ignored Ctrl-C.

 How? : when the precise exception(s) concerned by the try is
 known, use them explicitely in the "with". Otherwise, let's use
 the pattern "with e when Errors.noncritical e -> "

 Particular case : when an exception is catched and reraised
 immediately after some adjustments, we leave it untouched.
 Simply, for easily identifying these situations later, the name
 of the exception variable is changed to "reraise".

 Please also adopt this coding style. Automatic checks based
 on the "mascot" tool of X. Clerc will be runned regularly.
 If you want to avoid to check a particular try...with, use
 the variable name "any" after the "with".

 All these changes have been tested using the standard library
 and the test-suite, but unfortunately this is far from ensuring
 that coqtop behaves as before. We'll see after the nightly bench...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7

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 *)