diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-13 13:49:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 21:56:56 +0200 |
| commit | 5ac6c86ad8e18161151d53687da1e2825f0a6b46 (patch) | |
| tree | c8503040a7ed852425fede1e1fc5a25755619383 /lib/cErrors.ml | |
| parent | 7ff42d43a6107dff984676902943ec32f187c40d (diff) | |
[pp] Try to properly tag error messages in cError.
In order to get proper coloring, we must tag the headers of error
messages in `CError`.
This should fix bug
https://coq.inria.fr/bugs/show_bug.cgi?id=5135
However, note that this could interact badly with the richpp printing
used by the IDE. At this level, we have no clue which tag we'd like to
apply, as we know (and shouldn't) nothing about the top level backend.
Thus, for now I've selected the console printer, hoping that the
`Richpp` won't crash the IDE.
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index c69c7e400..5c56192fc 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -16,6 +16,16 @@ let push = Backtrace.add_backtrace exception Anomaly of string option * std_ppcmds (* System errors *) +(* XXX: To move to common tagging functions in Pp, blocked on tag + * system cleanup as we cannot define generic error tags now. + * + * Anyways, tagging should not happen here, but in the specific + * listener to the msg_* stuff. + *) +let tag_err_str s = tag Ppstyle.(Tag.inj error_tag tag) (str s) ++ spc () +let err_str = tag_err_str "Error:" +let ann_str = tag_err_str "Anomaly:" + let _ = let pr = function | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"") @@ -93,7 +103,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + hov 0 (ann_str ++ raw_anomaly e ++ spc () ++ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else @@ -115,7 +125,7 @@ let iprint_no_report (e, info) = let _ = register_handler begin function | UserError(s, pps) -> - hov 0 (str "Error: " ++ where (Some s) ++ pps) + hov 0 (err_str ++ where (Some s) ++ pps) | _ -> raise Unhandled end |