diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:28 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:28 +0000 |
commit | 8aa2e600d375caffef47058f1d095777a0dfdbb0 (patch) | |
tree | 4793804a7f01b34a7e95c3001ccbd9d7f57e4763 /library/library.ml | |
parent | 1126ec7c771e18644c361fcdf1f8d59d6b7f73e7 (diff) |
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
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 34 |
1 files changed, 15 insertions, 19 deletions
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 *) |