uniformisation messages d'erreur

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

1 files changed, 48 insertions, 44 deletions

diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 5b451046c8..c72f2ddb3c 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -19,60 +19,64 @@ let guill s = "\""^s^"\""
 let where s =
   if !Options.debug then  [< 'sTR"in "; 'sTR s; 'sTR":"; 'sPC >] else [<>]
 
+let report () = [< 'sTR "."; 'sPC; 'sTR "Please report." >]
+
 (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
 let rec explain_exn_default = function
-  | Stream.Failure -> [< 'sTR"Error: uncaught Parse.Failure." >]
-  | Stream.Error txt -> hOV 0 [< 'sTR"Syntax error: "; 'sTR txt >]
-  | Token.Error txt -> hOV 0 [< 'sTR"Lexer error: "; 'sTR txt >]
-  | Sys_error msg -> hOV 0 [< 'sTR"OS error: " ; 'sTR msg >]
-  | UserError(s,pps) -> hOV 1 [< 'sTR"Error: "; where s; pps >]
-	
-  | Out_of_memory -> [< 'sTR"Out of memory" >]
-  | Stack_overflow -> [< 'sTR"Stack overflow" >]
-	  
-  | Ast.No_match s -> hOV 0 [< 'sTR"Ast matching error : "; 'sTR s >]
-	
-  | Anomaly (s,pps) -> hOV 1 [< 'sTR"System Anomaly: "; where s; pps >]
-	  
+  | Stream.Failure -> 
+      hOV 0 [< 'sTR "Anomaly: Uncaught Stream.Failure." >]
+  | Stream.Error txt -> 
+      hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
+  | Token.Error txt -> 
+      hOV 0 [< 'sTR "Syntax error: "; 'sTR txt >]
+  | Sys_error msg -> 
+      hOV 0 [< 'sTR "Error: OS: "; 'sTR msg >]
+  | UserError(s,pps) -> 
+      hOV 1 [< 'sTR"Error: "; where s; pps >]
+  | Out_of_memory -> 
+      hOV 0 [< 'sTR "Out of memory" >]
+  | Stack_overflow -> 
+      hOV 0 [< 'sTR "Stack overflow" >]
+  | Ast.No_match s -> 
+      hOV 0 [< 'sTR "Anomaly: Ast matching error: "; 'sTR s >]
+  | Anomaly (s,pps) -> 
+      hOV 1 [< 'sTR "Anomaly: "; where s; pps; report () >]
   | Match_failure(filename,pos1,pos2) ->
-      hOV 1 [< 'sTR"Match failure in file " ;
-	       'sTR filename ; 'sTR " from char #" ;
-	       'iNT pos1 ; 'sTR " to #" ; 'iNT pos2 >]
-
-  | Not_found -> [< 'sTR"Search error." >]
-
-  | Failure s -> hOV 0 [< 'sTR "System Error (Failure): " ; 'sTR (guill s) >]
-
-  | Invalid_argument s -> hOV 0 [< 'sTR"Invalid argument: " ; 'sTR (guill s) >]
-
-  | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
-
-  | TypeError(k,ctx,te) -> hOV 0 (Himsg.explain_type_error k ctx te)
-
-  | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
-
-  | Logic.RefinerError e -> hOV 0 (Himsg.explain_refiner_error e)
-
+      hOV 1 [< 'sTR "Anomaly: Match failure in file ";
+	       'sTR (guill filename); 'sTR " from char #";
+	       'iNT pos1; 'sTR " to #"; 'iNT pos2;
+	       report () >]
+  | Not_found -> 
+      hOV 0 [< 'sTR "Anomaly: Search error"; report () >]
+  | Failure s -> 
+      hOV 0 [< 'sTR "Anomaly: Failure "; 'sTR (guill s); report () >]
+  | Invalid_argument s -> 
+      hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >]
+  | Sys.Break -> 
+      hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
+  | TypeError(k,ctx,te) -> 
+      hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >]
+  | InductiveError e -> 
+      hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
+  | Logic.RefinerError e -> 
+      hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_refiner_error e >]
   | Tacmach.FailError i ->
-    hOV 0 [< 'sTR"Fail tactic always fails (level "; 'iNT i; 'sTR")." >]
-
+      hOV 0 [< 'sTR "Error: Fail tactic always fails (level "; 
+	       'iNT i; 'sTR")." >]
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
                explain_exn_default exc >]
-
-  | Lexer.Error Illegal_character -> [< 'sTR "Illegal character." >]
-	
-  | Lexer.Error Unterminated_comment -> [< 'sTR "Unterminated comment." >]
-	
-  | Lexer.Error Unterminated_string -> [< 'sTR "Unterminated string." >]
-	
+  | Lexer.Error Illegal_character -> 
+      hOV 0 [< 'sTR "Syntax error: Illegal character." >]
+  | Lexer.Error Unterminated_comment -> 
+      hOV 0 [< 'sTR "Syntax error: Unterminated comment." >]
+  | Lexer.Error Unterminated_string -> 
+      hOV 0 [< 'sTR "Syntax error: Unterminated string." >]
   | reraise ->
-      flush_all();
-      (try Printexc.print raise reraise with _ -> ());
-      flush_all();
-      [< 'sTR "Please report." >]
+      hOV 0 [< 'sTR "Anomaly: Uncaught exception "; 
+	       'sTR (Printexc.to_string reraise); report () >]
 
 let raise_if_debug e =
   if !Options.debug then raise e