diff options
| -rw-r--r-- | lib/cErrors.ml | 14 | ||||
| -rw-r--r-- | parsing/cLexer.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 3 | ||||
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rw-r--r-- | test-suite/output/ltac.out | 3 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
7 files changed, 19 insertions, 9 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 diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 79771f3f6..a0cf631ea 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -105,7 +105,7 @@ module Error = struct Printf.sprintf "Unsupported Unicode character (0x%x)" x) (* Require to fix the Camlp4 signature *) - let print ppf x = Pp.pp_with ppf (Pp.str (to_string x)) + let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x)) end open Error diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 41eb5826b..cf9a42945 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -112,8 +112,7 @@ let guard_term ch1 s i = match s.[i] with (* The call 'guard s i' should return true if the contents of s *) (* starting at i need bracketing to avoid ambiguities. *) let pr_guarded guard prc c = - msg_with Format.str_formatter (prc c); - let s = Format.flush_str_formatter () ^ "$" in + let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) let pr_constr = pr_constr diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b99d80e95..ba85286dd 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index a7bde5ea3..1ff09e3af 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,6 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f0f8f1864..e9771cfa4 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -13,7 +13,7 @@ open Flags open Vernac open Pcoq -let top_stderr x = msg_with !Pp_control.err_ft x +let top_stderr x = msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft x (* A buffer for the character read from a channel. We store the command * entered to be able to report errors without pretty-printing. *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b453dbc46..de45090bf 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -143,7 +143,7 @@ let pr_new_syntax_in_context loc chan_beautify ocom = | None -> mt() in let after = comment (CLexer.extract_comments (snd loc)) in if !beautify_file then - Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + Pp.msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (hov 0 (before ++ com ++ after)) else Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; @@ -181,7 +181,7 @@ let pp_cmd_header loc com = and take control of the console. *) let print_cmd_header loc com = - Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); + Pp.pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () let rec interp_vernac po chan_beautify checknav (loc,com) = |