From d1569f060a114b113ea9f326f1dec1c1e3f101dc Mon Sep 17 00:00:00 2001 From: Regis-Gianas Date: Tue, 4 Nov 2014 22:50:00 +0100 Subject: printing/Ppannotation: New annotation for tactic syntactic objects. printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services. --- printing/richPrinter.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'printing/richPrinter.ml') diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml index 07e97668c..66732319c 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) -- cgit v1.2.3