summaryrefslogtreecommitdiff
path: root/lib/errors.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /lib/errors.ml
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'lib/errors.ml')
-rw-r--r--lib/errors.ml79
1 files changed, 79 insertions, 0 deletions
diff --git a/lib/errors.ml b/lib/errors.ml
new file mode 100644
index 00000000..6affea23
--- /dev/null
+++ b/lib/errors.ml
@@ -0,0 +1,79 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+open Pp
+
+(* spiwack: it might be reasonable to decide and move the declarations
+ of Anomaly and so on to this module so as not to depend on Util. *)
+
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+(** [print_gen] is a general exception printer which tries successively
+ all the handlers of a list, and finally a [bottom] handler if all
+ others have failed *)
+
+let rec print_gen bottom stk e =
+ match stk with
+ | [] -> bottom e
+ | h::stk' ->
+ try h e
+ with
+ | Unhandled -> print_gen bottom stk' e
+ | any -> print_gen bottom stk' any
+
+(** Only anomalies should reach the bottom of the handler stack.
+ In usual situation, the [handle_stack] is treated as it if was always
+ non-empty with [print_anomaly] as its bottom handler. *)
+
+let where s =
+ if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
+
+let raw_anomaly e = match e with
+ | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
+ | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
+ | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
+
+let print_anomaly askreport e =
+ if askreport then
+ hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+ else
+ hov 0 (raw_anomaly e)
+
+(** The standard exception printer *)
+let print e = print_gen (print_anomaly true) !handle_stack e
+
+(** Same as [print], except that the "Please report" part of an anomaly
+ isn't printed (used in Ltac debugging). *)
+let print_no_report e = print_gen (print_anomaly false) !handle_stack e
+
+(** Same as [print], except that anomalies are not printed but re-raised
+ (used for the Fail command) *)
+let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
+
+(** Predefined handlers **)
+
+let _ = register_handler begin function
+ | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
+ | _ -> raise Unhandled
+end
+
+(** Critical exceptions shouldn't be catched and ignored by mistake
+ by inner functions during a [vernacinterp]. They should be handled
+ only at the very end of interp, to be displayed to the user. *)
+
+(** NB: in the 8.4 branch, for maximal compatibility, anomalies
+ are considered non-critical *)
+
+let noncritical = function
+ | Sys.Break | Out_of_memory | Stack_overflow -> false
+ | _ -> true
+