From 7ff42d43a6107dff984676902943ec32f187c40d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 13 Oct 2016 13:44:35 +0200 Subject: [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. --- plugins/ssrmatching/ssrmatching.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ssrmatching') 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 *) -- cgit v1.2.3 From cb5f55380875bb3029b051eb3acfbb912d83454b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 13 Oct 2016 14:21:22 +0200 Subject: [pp] Use more convenient pp API in ssrmatching --- plugins/ssrmatching/ssrmatching.ml4 | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 4d1ac7139..21606b2d6 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 ~pp_tag:Ppstyle.pp_tag 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 -- cgit v1.2.3