diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-13 13:44:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-18 21:56:50 +0200 |
| commit | 7ff42d43a6107dff984676902943ec32f187c40d (patch) | |
| tree | 8c488cb2a8752144c3a744203129001bf3a2959e /plugins/ssrmatching | |
| 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.
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae..4d1ac7139 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 *) |