diff options
| -rw-r--r-- | lib/clib.mllib | 2 | ||||
| -rw-r--r-- | lib/richpp.ml (renamed from lib/richPp.ml) | 0 | ||||
| -rw-r--r-- | lib/richpp.mli (renamed from lib/richPp.mli) | 0 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 2 | ||||
| -rw-r--r-- | printing/pptactic.ml | 6 | ||||
| -rw-r--r-- | printing/pptactic.mli | 2 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 2 | ||||
| -rw-r--r-- | printing/printing.mllib | 2 | ||||
| -rw-r--r-- | printing/richPrinter.ml | 26 | ||||
| -rw-r--r-- | printing/richprinter.ml | 26 | ||||
| -rw-r--r-- | printing/richprinter.mli (renamed from printing/richPrinter.mli) | 6 |
13 files changed, 41 insertions, 41 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib index 568ffbe0e..3fee88854 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -32,7 +32,7 @@ Pp Xml_lexer Xml_parser Xml_printer -RichPp +Richpp CUnix Envars Aux_file diff --git a/lib/richPp.ml b/lib/richpp.ml index f9a7e83a8..f9a7e83a8 100644 --- a/lib/richPp.ml +++ b/lib/richpp.ml diff --git a/lib/richPp.mli b/lib/richpp.mli index 834115d40..834115d40 100644 --- a/lib/richPp.mli +++ b/lib/richpp.mli diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c36ee21eb..9ee81b278 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -812,7 +812,7 @@ include Make (struct let tag_constr_expr = do_not_tag end) -module RichPp (Indexer : sig +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) = struct diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index d2877edc5..5f8b2f736 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -20,6 +20,6 @@ include Ppconstrsig.Pp Please refer to {!RichPp} to know what are the requirements over [Indexer.index] behavior. *) -module RichPp (Indexer : sig val index : Ppannotation.t -> string end) +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) : Ppconstrsig.Pp diff --git a/printing/pptactic.ml b/printing/pptactic.ml index ad3f95ef2..44f4b456c 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1339,14 +1339,14 @@ let _ = Hook.set Tactic_debug.match_rule_printer pr_match_rule false (pr_glob_tactic (Global.env())) (fun (_,p) -> pr_constr_pattern p) rl) -module RichPp (Indexer : sig +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) = struct - include Make (Ppconstr.RichPp (Indexer)) (struct + include Make (Ppconstr.Richpp (Indexer)) (struct open Ppannotation open Indexer - let tag_keyword = Pp.tag (Indexer.index AKeyword) + let tag_keyword = Pp.tag (Indexer.index AKeyword) let tag_glob_tactic_expr e = Pp.tag (index (AGlobTacticExpr e)) let tag_glob_atomic_tactic_expr a = Pp.tag (index (AGlobAtomicTacticExpr a)) let tag_raw_tactic_expr e = Pp.tag (index (ARawTacticExpr e)) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 36d116f1a..2003cc1e1 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -64,6 +64,6 @@ include Pptacticsig.Pp Please refer to {!RichPp} to know what are the requirements over [Indexer.index] behavior. *) -module RichPp (Indexer : sig val index : Ppannotation.t -> string end) +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) : Pptacticsig.Pp diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8814daf70..21fac8a35 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1272,13 +1272,13 @@ include Make (Ppconstr) (Pptactic) (struct let tag_vernac = do_not_tag end) -module RichPp (Indexer : sig +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) = struct include Make - (Ppconstr.RichPp (Indexer)) - (Pptactic.RichPp (Indexer)) + (Ppconstr.Richpp (Indexer)) + (Pptactic.Richpp (Indexer)) (struct open Ppannotation let tag_keyword = Pp.tag (Indexer.index AKeyword) diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 616fc7345..06f51f060 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -20,5 +20,5 @@ include Ppvernacsig.Pp Please refer to {!RichPp} to know what are the requirements over [Indexer.index] behavior. *) -module RichPp (Indexer : sig val index : Ppannotation.t -> string end) +module Richpp (Indexer : sig val index : Ppannotation.t -> string end) : Ppvernacsig.Pp diff --git a/printing/printing.mllib b/printing/printing.mllib index 791070298..652a34fa1 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -10,4 +10,4 @@ Printmod Prettyp Ppvernac Ppvernacsig -RichPrinter +Richprinter diff --git a/printing/richPrinter.ml b/printing/richPrinter.ml deleted file mode 100644 index 66732319c..000000000 --- a/printing/richPrinter.ml +++ /dev/null @@ -1,26 +0,0 @@ -open RichPp - -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 make_richpp pr ast = - let raw_pp, rich_pp = - rich_pp Indexer.get_annotations (fun () -> pr ast) - in - let xml = Ppannotation.( - xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp - ) - 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) diff --git a/printing/richprinter.ml b/printing/richprinter.ml new file mode 100644 index 000000000..d27b7c373 --- /dev/null +++ b/printing/richprinter.ml @@ -0,0 +1,26 @@ +open Richpp + +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 make_richpp pr ast = + let raw_pp, rich_pp = + rich_pp Indexer.get_annotations (fun () -> pr ast) + in + let xml = Ppannotation.( + xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp + ) + 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) diff --git a/printing/richPrinter.mli b/printing/richprinter.mli index 9d02ad294..6df5c9c6a 100644 --- a/printing/richPrinter.mli +++ b/printing/richprinter.mli @@ -14,9 +14,9 @@ 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 + document contains a [startpos] and an [endpos] attribute that relate this node to the raw pretty-printing. - Please refer to {!RichPp} for more details. *) + Please refer to {!Richpp} for more details. *) (** A rich pretty-print is composed of: *) type rich_pp = @@ -25,7 +25,7 @@ type rich_pp = (** - a generalized semi-structured document whose attributes are annotations ; *) - * Ppannotation.t RichPp.located Xml_datatype.gxml + * Ppannotation.t Richpp.located Xml_datatype.gxml (** - an XML document, representing annotations as usual textual XML attributes. *) |