diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-31 17:18:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-02 11:36:41 +0100 |
| commit | 565a9a1b5368c586e529fc9774e4cb4b81c6441b (patch) | |
| tree | 054160a2e7eb5842f8b5e6b7c20fa016b8ae1817 /printing/genprint.mli | |
| parent | b0e9d691d6c48fb09b20bb9d98626143eb8b92df (diff) | |
Setting a system to register printers for Ltac values.
The model provides three kinds of printers depending on whether the
printer needs a context, and, if yes if it supports levels. In the
latter case, it takes defaults levels for printing when in a
surrounded context (lconstr style) and for printing when not in a
surrounded context (constr style).
This model preserves the 8.7 focussing semantics of "idtac"
(i.e. focussing only when an env is needed) but it also shows that the
semantics of "idtac", which focusses the goal depending on the type of
its arguments, is a bit ad hoc to understand.
See discussion at PR#6047
"https://github.com/coq/coq/pull/6047#discussion_r148278454".
Diffstat (limited to 'printing/genprint.mli')
| -rw-r--r-- | printing/genprint.mli | 31 |
1 files changed, 23 insertions, 8 deletions
diff --git a/printing/genprint.mli b/printing/genprint.mli index 76d80f3b5..2da9bbc36 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,22 +10,37 @@ open Genarg +type printer_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 } + +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 -val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t +type 'a top_printer = 'a -> printer_result + +val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) -val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb printer (** Printer for glob level generic arguments. *) -val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) -val generic_raw_print : rlevel generic_argument printer -val generic_glb_print : glevel generic_argument printer -val generic_top_print : tlevel generic_argument printer - val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> 'top printer -> unit + 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit +val register_val_print0 : 'top Geninterp.Val.typ -> + 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> 'raw printer -> unit + +val generic_raw_print : rlevel generic_argument printer +val generic_glb_print : glevel generic_argument printer +val generic_top_print : tlevel generic_argument top_printer +val generic_val_print : Geninterp.Val.t top_printer |