The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Unfortunately, it seems no information is exported to XML after rich pretty-printing:

https://github.com/coq/coq/blob/trunk/printing/ppannotation.ml

First, the annotation type is quite restricted. Second, the annotation attributes are never exported, as of now.

- Valentin

On Fri, Aug 14, 2015 at 11:21 PM Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Sat, Aug 15, 2015 at 01:58:16AM +0000, Valentin Robert wrote:
> To the extent of my investigation, I believe that:
> - the PrintAST command of the new XML protocol prints AST information for
> Vernacular commands that were sent to the interpreter, but cannot give
> information about the current Gallina context ;

Right.

I did not try myself for lack of time, but with the new pretty printer
infrastructure it should be possible to enrich the output with extra
information collected during the constr->glob_constr->constr_expr chain.
I think the only example is the new color-thing in error messages, so
I'd start looking at it.

> It seems though that the only way to recover the "notation to low-level"
> mapping is to use the glob_constr type, and recursively query for possible
> notations using Notation.uninterp_notations and pattern matching the
> interpretation term (a notation_constr term) with the glob_constr I have to
> figure out which notation matches and how much of the glob_constr is part
> of the notation.

Note that the transformation chain above does roughly what you say, so
ideally you just have to record some metadata during the transformation.

Best
--
Enrico Tassi