diff options
Diffstat (limited to 'printing/richPrinter.ml')
| -rw-r--r-- | printing/richPrinter.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml index 07e97668c6..66732319cc 100644 --- a/printing/richPrinter.ml +++ b/printing/richPrinter.ml @@ -4,15 +4,16 @@ module Indexer = Indexer (struct type t = Ppannotation.t end) module RichPpConstr = Ppconstr.RichPp (Indexer) module RichPpVernac = Ppvernac.RichPp (Indexer) +module RichPpTactic = Pptactic.RichPp (Indexer) type rich_pp = string * Ppannotation.t RichPp.located Xml_datatype.gxml * Xml_datatype.xml -let richpp_vernac phrase_ast = +let make_richpp pr ast = let raw_pp, rich_pp = - rich_pp Indexer.get_annotations (fun () -> RichPpVernac.pr_vernac phrase_ast) + rich_pp Indexer.get_annotations (fun () -> pr ast) in let xml = Ppannotation.( xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp @@ -20,3 +21,6 @@ let richpp_vernac phrase_ast = in (raw_pp, rich_pp, xml) +let richpp_vernac = make_richpp RichPpVernac.pr_vernac +let richpp_constr = make_richpp RichPpConstr.pr_constr_expr +let richpp_tactic env = make_richpp (RichPpTactic.pr_tactic env) |