diff options
| author | Emilio Jesus Gallego Arias | 2016-06-01 17:52:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:47:13 +0100 |
| commit | 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 (patch) | |
| tree | ee3b8a94a6414e7c12920ce445f1157796ad5ecf /printing/ppannotation.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/ppannotation.mli')
| -rw-r--r-- | printing/ppannotation.mli | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli deleted file mode 100644 index b0e0facef6..0000000000 --- a/printing/ppannotation.mli +++ /dev/null @@ -1,29 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** This module defines the annotations that are attached to - semi-structured pretty-printing of Coq syntactic objects. *) - -open Ppextend -open Constrexpr -open Vernacexpr -open Genarg - -type t = - | AKeyword - | AUnparsing of unparsing - | AConstrExpr of constr_expr - | AVernac of vernac_expr - | AGlbGenArg of glob_generic_argument - | ARawGenArg of raw_generic_argument - -val tag_of_annotation : t -> string - -val attributes_of_annotation : t -> (string * string) list - -val tag : t Pp.Tag.key |