printing/RichPrinter: New API for rich pretty-printing.

printing/Ppannotation: Define the projection of annotations into XML attributes.
lib/richPp: Implements valid entities escaping.

5 files changed, 65 insertions, 0 deletions

diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index 3274a7bdcf..b739dcaeb9 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -14,3 +14,11 @@ type t =
   | AUnparsing  of unparsing
   | AConstrExpr of constr_expr
   | AVernac     of vernac_expr
+
+let tag_of_annotation = function
+  | AUnparsing _  -> "unparsing"
+  | AConstrExpr _ -> "constr_expr"
+  | AVernac _     -> "vernac_expr"
+
+let attributes_of_annotation a =
+  []
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index a462c9f335..38b09eef0c 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -17,3 +17,7 @@ type t =
   | AUnparsing  of unparsing
   | AConstrExpr of constr_expr
   | AVernac     of vernac_expr
+
+val tag_of_annotation : t -> string
+
+val attributes_of_annotation : t -> (string * string) list
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 01c835d898..713c2dee6f 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -9,3 +9,4 @@ Printmod
 Prettyp
 Ppvernac
 Ppvernacsig
+RichPrinter
diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml
new file mode 100644
index 0000000000..5249691e1f
--- /dev/null
+++ b/printing/richPrinter.ml
@@ -0,0 +1,17 @@
+open RichPp
+
+module Indexer = Indexer (struct type t = Ppannotation.t end)
+
+module RichPpConstr = Ppconstr.RichPp (Indexer)
+module RichPpVernac = Ppvernac.RichPp (Indexer)
+
+let richpp_vernac phrase_ast =
+  let raw_pp, rich_pp =
+    rich_pp Indexer.get_annotations (fun () -> RichPpVernac.pr_vernac phrase_ast)
+  in
+  let xml = Ppannotation.(
+    xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
+  )
+  in
+  (raw_pp, rich_pp, xml)
+
diff --git a/printing/richPrinter.mli b/printing/richPrinter.mli
new file mode 100644
index 0000000000..2f97cc3fe2
--- /dev/null
+++ b/printing/richPrinter.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** This module provides an entry point to "rich" pretty-printers that
+    produce pretty-printing as done by {!Printer} but with additional
+    annotations represented as a semi-structured document.
+
+    To understand what are these annotations and how they are represented
+    as standard XML attributes, please refer to {!Ppannotation}.
+
+    In addition to these annotations, each node of the semi-structured
+    document contains a [startpos] and an [endpos] attributes that
+    relate this node to the raw pretty-printing.
+    Please refer to {!RichPp} for more details. *)
+
+(** A rich pretty-print is composed of: *)
+type rich_pp =
+    (** - a raw pretty-print ; *)
+    string
+
+    (** - a generalized semi-structured document whose attributes are
+        annotations ; *)
+    * Ppannotation.t RichPp.located Xml_datatype.gxml
+
+    (** - an XML document, representing annotations as usual textual
+        XML attributes. *)
+    * Xml_datatype.xml
+
+(** [richpp_vernac phrase] produces a rich pretty-printing of [phrase]. *)
+val richpp_vernac : Vernac.vernac_expr -> rich_pp