diff options
| author | Maxime Dénès | 2017-12-08 10:17:20 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-08 10:17:20 +0100 |
| commit | 6d34fbc12186390da382819f06857c6e2d5d9cd1 (patch) | |
| tree | 1cfe9995b90eb1bbe68a30bcec1d56d9c0b80e5e /printing/pputils.ml | |
| parent | f96262f9c56c0ce164e316c916b76bf0bdbae731 (diff) | |
| parent | 9113815578286d1d887df48f4f03870d2d8a128c (diff) | |
Merge PR #6158: Allows a level in the raw and glob printers
Diffstat (limited to 'printing/pputils.ml')
| -rw-r--r-- | printing/pputils.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml index 12d5338ade..a544b47623 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 |