uniformisation messages d'erreur

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

7 files changed, 65 insertions, 63 deletions

diff --git a/TODO b/TODO
index ab06eb477..2e3e01b41 100644
--- a/TODO
+++ b/TODO
@@ -7,7 +7,6 @@ Distribution:
 Environnement:
 
 - Porter SearchIsos
-- Require synchronisé
 - Interdire de faire 2 fois la même définition avec le même nom absolu FAIT
 
 Tactiques:
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 9f03ccc1e..25578ad76 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -206,7 +206,7 @@ let pr_context_unlimited env =
 
 let pr_ne_context_of header k env =
   if Environ.context env = empty_context then [< >]
-  else let penv = pr_context_unlimited env in [< header; penv >]
+  else let penv = pr_context_unlimited env in [< header; penv; 'fNL >]
 
 let pr_context_limit n env =
   let named_context = Environ.named_context env in
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 5b451046c..c72f2ddb3 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
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index aa4f719c5..d3c4c41fe 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -21,15 +21,15 @@ let guill s = "\""^s^"\""
 
 let explain_unbound_rel k ctx n =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in
-  [< 'sTR"Unbound reference: "; pe; 'fNL;
+  let pe = pr_ne_context_of [< 'sTR "In environment" >] k ctx in
+  [< 'sTR"Unbound reference: "; pe;
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
 
 let explain_not_type k ctx j =
   let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of [< 'sTR"In environment" >] k ctx in
   let pc,pt = prjudge_env ctx j in
-  [< pe; 'fNL; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
+  [< pe; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
      'sTR"has type"; 'sPC; pt; 'sPC; 
      'sTR"which should be Set, Prop or Type." >];;
 
@@ -92,21 +92,21 @@ let explain_ill_formed_branch k ctx c i actty expty =
 
 let explain_generalization k ctx (name,var) j =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR "In environment" >] k ctx in
   let pv = prtype_env ctx var in
   let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
-  [< 'sTR"Illegal generalization: "; pe; 'fNL;
+  [< 'sTR"Illegal generalization: "; pe;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sTR","; 'sPC; 'sTR"it has type"; 'sPC; pt; 
      'sPC; 'sTR"which should be Set, Prop or Type." >]
 
 let explain_actual_type k ctx c ct pt =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_context_of [< 'sTR"In environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR "In environment" >] k ctx in
   let pc = prterm_env ctx c in
   let pct = prterm_env ctx ct in
   let pt = prterm_env ctx pt in
-  [< pe; 'fNL;
+  [< pe;
      'sTR "The term"; 'bRK(1,1); pc ; 'sPC ;
      'sTR "has type" ; 'bRK(1,1); pct; 'bRK(1,1); 
      'sTR "while it is expected to have type"; 'bRK(1,1); pt >]
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b127159b1..9fe9142c1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -97,8 +97,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in     
   let idps,typs = List.split ps in      
   let idfs,tyfs = List.split fs in
-  if not (free_in_asts idstruc tyfs) then 
-    message "Error: A record cannot be recursive";
+  if not (free_in_asts idstruc tyfs) then error "A record cannot be recursive";
   let newps,newfs = typecheck_params_and_field ps fs in
   let app_constructor = 
     ope("APPLISTEXPL",
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 9b7250a4e..35dde0bcf 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -217,7 +217,7 @@ let print_toplevel_error exc =
 	mSGERRNL [<>]; pp_flush(); exit 0
     | Vernacinterp.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise Vernacinterp.Drop;
-        [< 'sTR"There is no ML toplevel."; 'fNL >]
+        [< 'sTR"Error: There is no ML toplevel."; 'fNL >]
     | Vernacinterp.ProtectedLoop ->
 	raise Vernacinterp.ProtectedLoop
     | Vernacinterp.Quit -> 
@@ -296,7 +296,7 @@ let rec coq_switch b =
     | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0
     | Vernacinterp.Quit -> exit 0
     | e ->
-	mSGERRNL [< 'sTR"Anomaly in the toplevel loop. Please report." >];
+	mSGERRNL [< 'sTR"Anomaly: toplevel loop. Please report." >];
 	coq_switch b
 
 let loop () = coq_switch true
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b57001237..0a7aa7862 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -752,15 +752,15 @@ let _ =
 		  ()
               with e ->
             	if is_unsafe "proof" then begin
-                  mSGNL [< 'sTR"Error: checking of theorem " ; pr_id s ;
-                           'sPC ; 'sTR"failed" ;
-                           'sTR"... converting to Axiom" >];
+                  mSGNL [< 'sTR "Warning: checking of theorem "; pr_id s;
+                           'sPC; 'sTR "failed";
+                           'sTR "... converting to Axiom" >];
                   delete_proof s;
                   parameter_def_var (string_of_id s) com
            	end else 
-		  errorlabstrm "vernacentries__TheoremProof"
-                    [< 'sTR"checking of theorem " ; pr_id s ; 'sPC ;
-                       'sTR"failed... aborting" >])
+		  errorlabstrm "Vernacentries.TheoremProof"
+                    [< 'sTR "checking of theorem "; pr_id s; 'sPC;
+                       'sTR "failed... aborting" >])
        | _ -> bad_vernac_args "TheoremProof")
 
 let _ =