diff options
author | 2013-03-12 23:59:28 +0000 | |
---|---|---|
committer | 2013-03-12 23:59:28 +0000 | |
commit | 8aa2e600d375caffef47058f1d095777a0dfdbb0 (patch) | |
tree | 4793804a7f01b34a7e95c3001ccbd9d7f57e4763 /kernel | |
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 'kernel')
-rw-r--r-- | kernel/names.ml | 2 | ||||
-rw-r--r-- | kernel/names.mli | 7 |
2 files changed, 5 insertions, 4 deletions
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. *) |