diff options
| author | Hugo Herbelin | 2017-11-07 16:26:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 18:08:05 +0100 |
| commit | be133d7bc92b67a6581a99f7aa679fb3a60ce57b (patch) | |
| tree | 2b0f757e0e0da637bfa96d2f94875aa8987c71f1 /API/API.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 'API/API.mli')
| -rw-r--r-- | API/API.mli | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/API/API.mli b/API/API.mli index 1f1b05eadb..2aa5da67da 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5217,16 +5217,20 @@ end module Genprint : sig - 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 - type 'a printer = 'a -> Pp.t - type 'a top_printer = 'a -> printer_result +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level + type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t + 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 register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> |