A new mechanism to handle errors.

Instead of the monolitic Cerrors, I introduce a lightweight Errors module
whose error message can be expanded by module introducing exceptions.

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

3 files changed, 85 insertions, 1 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
new file mode 100644
index 000000000..89e924948
--- /dev/null
+++ b/lib/errors.ml
@@ -0,0 +1,56 @@
+(***********************************************************************)
+(*  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. *)
+(* spiwack: This module contains stuff exfiltrated from Cerrors. *)
+
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+(* spiwack: [anomaly_string] and [report_fn] are copies from Cerrors.
+   Ultimately they should disapear from Cerrors. *)
+let anomaly_string () = str "Anomaly: "
+let report_fn () = (str "." ++ spc () ++ str "Please report.")
+(* [print_unhandled_exception] is the virtual bottom of the stack:
+   the [handle_stack] is treated as it if was always non-empty
+   with [print_unhandled_exception] as its last handler. *)
+let print_unhandled_exception e =
+  hov 0 (anomaly_string () ++ str "Uncaught exception " ++
+	 str (Printexc.to_string e) ++ report_fn ())
+
+let rec print_gen s e =
+  match s with
+  | [] -> print_unhandled_exception e
+  | h::s' ->
+    try h e
+    with
+    | Unhandled -> print_gen s' e
+    | e' -> print_gen s' e'
+
+let print e = print_gen !handle_stack e
+
+
+(*** Predefined handlers ***)
+
+let where s =
+  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+
+let _ = register_handler begin function
+  | Util.UserError(s,pps) ->
+      hov 0 (str "Error: " ++ where s ++ pps)
+  | Util.Anomaly (s,pps) ->
+      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+  | _ -> raise Unhandled
+end
+
diff --git a/lib/errors.mli b/lib/errors.mli
new file mode 100644
index 000000000..120634e60
--- /dev/null
+++ b/lib/errors.mli
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(** This modules implements basic manipulations of errors for use
+    throughout Coq's code. *)
+
+(** [register_handler h] registers [h] as a handler.
+    When an expression is printed with [print e], it
+    goes through all registered handles (the most
+    recent first) until a handle deals with it.
+
+    Handles signal that they don't deal with some exception
+    by raisine [Unhandled].
+
+    Handles can raise exceptions themselves, in which
+    case, the exception is passed to the handles which
+    were registered before. *)
+exception Unhandled
+
+val register_handler : (exn -> Pp.std_ppcmds) -> unit
+
+val print : exn -> Pp.std_ppcmds
diff --git a/lib/lib.mllib b/lib/lib.mllib
index cfbedcc52..84180fc46 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -5,6 +5,7 @@ Flags
 Segmenttree
 Unicodetable
 Util
+Errors
 Bigint
 Hashcons
 Dyn
@@ -23,4 +24,4 @@ Heap
 Option
 Dnet
 Store
-Unionfind
\ No newline at end of file
+Unionfind