diff options
Diffstat (limited to 'printing/richPrinter.ml')
| -rw-r--r-- | printing/richPrinter.ml | 17 |
1 files changed, 17 insertions, 0 deletions
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) + |