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/printing.mllib | |
| 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/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index b0141b6d3..86b68d8fb 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,6 +1,5 @@ Genprint Pputils -Ppannotation Ppconstr Printer Printmod |