diff options
Diffstat (limited to 'toplevel/cerrors.ml')
| -rw-r--r-- | toplevel/cerrors.ml | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 40d74256..0983463a 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 10410 2007-12-31 13:11:55Z msozeau $ *) +(* $Id: cerrors.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -34,21 +34,21 @@ let rec explain_exn_default_aux anomaly_string report_fn = function | Stream.Failure -> hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.") | Stream.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) + hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Token.Error txt -> - hov 0 (str "Syntax error: " ++ str txt) + hov 0 (str "Syntax error: " ++ str txt ++ str ".") | Sys_error msg -> hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ()) | UserError(s,pps) -> - hov 1 (str "User error: " ++ where s ++ pps) + hov 0 (str "Error: " ++ where s ++ pps) | Out_of_memory -> - hov 0 (str "Out of memory") + hov 0 (str "Out of memory.") | Stack_overflow -> - hov 0 (str "Stack overflow") + hov 0 (str "Stack overflow.") | Anomaly (s,pps) -> - hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ()) + hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ()) | Match_failure(filename,pos1,pos2) -> - hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ + hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ if Sys.ocaml_version = "3.06" then (str " from character " ++ int pos1 ++ str " to " ++ int pos2) @@ -83,6 +83,11 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e) | RecursionSchemeError e -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e) + | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () -> + explain_exn_default_aux anomaly_string report_fn exc + | Proof_type.LtacLocated (s,exc) -> + hov 0 (Himsg.explain_ltac_call_trace s ++ fnl () + ++ explain_exn_default_aux anomaly_string report_fn exc) | Cases.PatternMatchingError (env,e) -> hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e) @@ -94,13 +99,15 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Error:" ++ spc () ++ str "The reference" ++ spc () ++ Libnames.pr_qualid q ++ spc () ++ str "was not found" ++ - spc () ++ str "in the current" ++ spc () ++ str "environment") + spc () ++ str "in the current" ++ spc () ++ str "environment.") | Nametab.GlobalizationConstantError q -> hov 0 (str "Error:" ++ spc () ++ - str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q) + str "No constant of this name:" ++ spc () ++ + Libnames.pr_qualid q ++ str ".") | Refiner.FailError (i,s) -> - hov 0 (str "Error: Tactic failure" ++ s ++ - if i=0 then mt () else str " (level " ++ int i ++ str").") + hov 0 (str "Error: Tactic failure" ++ + (if s <> mt() then str ":" ++ s else mt ()) ++ + if i=0 then str "." else str " (level " ++ int i ++ str").") | Stdpp.Exc_located (loc,exc) -> hov 0 ((if loc = dummy_loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) @@ -145,7 +152,7 @@ let raise_if_debug e = let _ = Tactic_debug.explain_logic_error := explain_exn_default let _ = Tactic_debug.explain_logic_error_no_anomaly := - explain_exn_default_aux (fun () -> mt()) (fun () -> mt()) + explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") let explain_exn_function = ref explain_exn_default |