From be133d7bc92b67a6581a99f7aa679fb3a60ce57b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 16:26:21 +0100 Subject: Extending further PR#6047 (system to register printers for Ltac values). We generalize the possible use of levels to raw and glob printers. This is potentially useful for printing ltac expressions which are the glob level. --- printing/pputils.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'printing/pputils.ml') diff --git a/printing/pputils.ml b/printing/pputils.ml index 12d5338ad..a544b4762 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -130,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) = let q = in_gen (rawwit wit2) q in hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q]) | ExtraArg s -> - Genprint.generic_raw_print (in_gen (rawwit wit) x) + let open Genprint in + match generic_raw_print (in_gen (rawwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = @@ -152,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = let ans = pr_sequence (pr_glb_generic env) [p; q] in hov_if_not_empty 0 ans | ExtraArg s -> - Genprint.generic_glb_print (in_gen (glbwit wit) x) + let open Genprint in + match generic_glb_print (in_gen (glbwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded -- cgit v1.2.3