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/genprint.mli | |
| 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/genprint.mli')
| -rw-r--r-- | printing/genprint.mli | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/printing/genprint.mli b/printing/genprint.mli index 2da9bbc36..baa60fcb2 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,19 +10,25 @@ open Genarg -type printer_with_level = +type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsContextAndLevel of printer_with_level +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level -type 'a printer = 'a -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t -type 'a top_printer = 'a -> printer_result +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) @@ -34,7 +40,7 @@ val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit + 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> |