diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-06-01 17:52:39 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-21 15:47:13 +0100 |
commit | 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 (patch) | |
tree | ee3b8a94a6414e7c12920ce445f1157796ad5ecf /printing/printmod.mli | |
parent | eda304d2f0531b8fa088a2d71d369d4482f29ed2 (diff) |
[pp] Remove unused printing tagging infrastructure.
Applications of it were not clear/unproven, it made printers more
complex (as they needed to be functors) and as it lacked examples it
confused some people.
The printers now tag unconditionally, it is up to the backends to
interpreted the tags.
Tagging (and indeed the notion of rich document) should be reworked in
a follow-up patch, so they are in sync, but this is a first step.
Tested, test-suite passes.
Notes:
- We remove the `Richprinter` module. It was only used in the
`annotate` IDE protocol call, its output was identical to the normal
printer (or even inconsistent if taggers were not kept manually in
sync).
- Note that Richpp didn't need a single change. In particular, its
main API entry point `Richpp.rich_pp` is not used by anyone.
Diffstat (limited to 'printing/printmod.mli')
-rw-r--r-- | printing/printmod.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/printing/printmod.mli b/printing/printmod.mli index 7f7d34392..f3079d5b6 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -6,9 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Pp open Names (** false iff the module is an element of an open module type *) val printable_body : DirPath.t -> bool -include Printmodsig.Pp +val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds +val print_module : bool -> module_path -> std_ppcmds +val print_modtype : module_path -> std_ppcmds |