From 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 17:52:39 +0200 Subject: [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. --- printing/printing.mllib | 1 - 1 file changed, 1 deletion(-) (limited to 'printing/printing.mllib') 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 -- cgit v1.2.3