diff options
| author |  Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:50:00 +0100 |
|---|---|---|
| committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
| commit | d1569f060a114b113ea9f326f1dec1c1e3f101dc (patch) | |
| tree | 68f4bfa95c003264511755ff266230ecefdd5e0d /printing/richPrinter.ml | |
| parent | 5076e90f880cdc3f085dd8d24f4722d0501d2518 (diff) | |
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.
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 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) |