diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 16:26:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:08:05 +0100 |
| commit | be133d7bc92b67a6581a99f7aa679fb3a60ce57b (patch) | |
| tree | 2b0f757e0e0da637bfa96d2f94875aa8987c71f1 /printing/pputils.ml | |
| parent | 1161ccf74578c3190d296dc37f39edecf28cf078 (diff) | |
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.
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 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 |