diff options
| author | Emilio Jesus Gallego Arias | 2016-10-13 13:44:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-10-18 21:56:50 +0200 |
| commit | 7ff42d43a6107dff984676902943ec32f187c40d (patch) | |
| tree | 8c488cb2a8752144c3a744203129001bf3a2959e | |
| parent | dff1450d43909e8aeaf8ce2db8bc19be42ee1ab1 (diff) | |
[pp] Add tagging function to all low-level printing calls.
The current tag system in `Pp` is generic, which implies we must choose
a tagging function when calling a printer.
For console printing there is a single choice, thus this commits adds it
a few missing cases.
| -rw-r--r-- | parsing/cLexer.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/coqloop.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
4 files changed, 5 insertions, 5 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 31025075cd..ff69bce886 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -96,7 +96,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 a34fa4cae7..4d1ac71394 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -112,7 +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); + msg_with ~pp_tag:Ppstyle.pp_tag Format.str_formatter (prc c); let s = Format.flush_str_formatter () ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index f0f8f18641..e9771cfa40 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 b453dbc469..de45090bfc 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) = |