summaryrefslogtreecommitdiff
path: root/toplevel/cerrors.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /toplevel/cerrors.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'toplevel/cerrors.ml')
-rw-r--r--toplevel/cerrors.ml33
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