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

6 files changed, 9 insertions, 14 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index af1330a42b..d6e88ed2c5 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -202,7 +202,7 @@ let declare_class_instance gr ctx params =
     (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
   Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
   new_instance_message ident typ def
-  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Cerrors.explain_exn e)
+  with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Errors.print e)
 
 let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
   match kind_of_term t with
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 737abb3f4a..831e27bed7 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -23,8 +23,6 @@ let print_loc loc =
 
 let guill s = "\""^s^"\""
 
-let where s =
-  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
 exception EvaluatedError of std_ppcmds * exn option
 
@@ -40,16 +38,12 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
   | Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
   | Sys_error msg ->
       hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
-  | UserError(s,pps) ->
-      hov 0 (str "Error: " ++ where s ++ pps)
   | Out_of_memory ->
       hov 0 (str "Out of memory.")
   | Stack_overflow ->
       hov 0 (str "Stack overflow.")
   | Timeout ->
       hov 0 (str "Timeout!")
-  | Anomaly (s,pps) ->
-      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | AnomalyOnError (s,exc) ->
       hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
 	fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
@@ -81,9 +75,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       msg
   | EvaluatedError (msg,Some reraise) ->
       msg ++ explain_exn_default_aux anomaly_string report_fn reraise
-  | reraise ->
-      hov 0 (anomaly_string () ++ str "Uncaught exception " ++
-	       str (Printexc.to_string reraise) ++ report_fn ())
+  | _ -> raise Errors.Unhandled
 
 let wrap_vernac_error strm =
   EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
@@ -165,6 +157,7 @@ let _ = Tactic_debug.explain_logic_error_no_anomaly :=
 let explain_exn_function = ref explain_exn_default
 
 let explain_exn e = !explain_exn_function e
+let _ = Errors.register_handler explain_exn
 
 let explain_exn_no_anomaly e =
    explain_exn_default_aux (fun () -> raise e) mt e
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 0dae61f4a6..2670160abf 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -13,7 +13,9 @@ open Util
 
 val print_loc : loc -> std_ppcmds
 
+(*
 val explain_exn : exn -> std_ppcmds
+*)
 
 (** Precompute errors raised during vernac interpretation *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e0f21aab87..c0f6894674 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -306,9 +306,9 @@ let parse_args arglist =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  msgnl (Cerrors.explain_exn e); exit 1
+	  msgnl (Errors.print e); exit 1
       end
-    | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
+    | e -> begin msgnl (Errors.print e); exit 1 end
 
 let init arglist =
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index a39e9c4292..72ebecfa70 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -510,7 +510,7 @@ let explain_exn e =
       | Error_in_file (s, _, inner) -> None,inner
       | _ -> None,e
   in
-  toploc,(Cerrors.explain_exn exc)
+  toploc,(Errors.print exc)
 
 let eval_call c =
   let rec handle_exn e =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ddf3ac6575..92e29c0421 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -309,7 +309,7 @@ let print_toplevel_error exc =
 	raise Vernacexpr.Quit
     | _ ->
 	(if is_pervasive_exn exc then (mt ()) else locstrm) ++
-        Cerrors.explain_exn exc
+        Errors.print exc
 
 (* Read the input stream until a dot is encountered *)
 let parse_to_dot =