From 6b69fc07f9f17e4d61dbb244c69f6c9de326e00f Mon Sep 17 00:00:00 2001 From: Yann Régis-Gianas Date: Wed, 5 Nov 2014 22:52:09 +0100 Subject: lib/RichPp: Rename into Richpp. printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics. --- lib/clib.mllib | 2 +- lib/richPp.ml | 186 ----------------------------------------------- lib/richPp.mli | 59 --------------- lib/richpp.ml | 186 +++++++++++++++++++++++++++++++++++++++++++++++ lib/richpp.mli | 59 +++++++++++++++ printing/ppconstr.ml | 2 +- printing/ppconstr.mli | 2 +- printing/pptactic.ml | 6 +- printing/pptactic.mli | 2 +- printing/ppvernac.ml | 6 +- printing/ppvernac.mli | 2 +- printing/printing.mllib | 2 +- printing/richPrinter.ml | 26 ------- printing/richPrinter.mli | 41 ----------- printing/richprinter.ml | 26 +++++++ printing/richprinter.mli | 41 +++++++++++ 16 files changed, 324 insertions(+), 324 deletions(-) delete mode 100644 lib/richPp.ml delete mode 100644 lib/richPp.mli create mode 100644 lib/richpp.ml create mode 100644 lib/richpp.mli delete mode 100644 printing/richPrinter.ml delete mode 100644 printing/richPrinter.mli create mode 100644 printing/richprinter.ml create mode 100644 printing/richprinter.mli diff --git a/lib/clib.mllib b/lib/clib.mllib index 568ffbe0ef..3fee888543 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 deleted file mode 100644 index f9a7e83a8e..0000000000 --- a/lib/richPp.ml +++ /dev/null @@ -1,186 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - incr count; - annotations := annotation :: !annotations; - string_of_int !count - - let get_annotations () = - let annotations = Array.of_list (List.rev !annotations) in - fun index -> annotations.(int_of_string index) - -end - -let rich_pp get_annotations ppcmds = - (** First, we use Format to introduce tags inside - the pretty-printed document. - - Each inserted tag is an index to an annotation. - *) - let tagged_pp = Format.( - - (** Warning: The following instructions are valid only if - [str_formatter] is not used for another purpose in - Pp.pp_with. *) - - let ft = str_formatter in - - (** We reuse {!Format} standard way of producing tags - inside pretty-printing. *) - pp_set_tags ft true; - - (** The whole output must be a valid document. To that - end, we nest the document inside a tag named . *) - pp_open_tag ft "pp"; - - (** XML ignores spaces. The problem is that our pretty-printings - are based on spaces to indent. To solve that problem, we - systematically output non-breakable spaces, which are properly - honored by XML. - - To do so, we reconfigure the [str_formatter] temporarily by - hijacking the function that output spaces. *) - let out, flush, newline, std_spaces = - pp_get_all_formatter_output_functions ft () - in - let set = pp_set_all_formatter_output_functions ft ~out ~flush ~newline in - set ~spaces:(fun k -> - for i = 0 to k - 1 do - Buffer.add_string stdbuf " " - done - ); - - (** Some characters must be escaped in XML. This is done by the - following rewriting of the strings held by pretty-printing - commands. *) - Pp.(pp_with ft (rewrite Xml_printer.pcdata_to_string (ppcmds ()))); - - (** Insert

. *) - pp_close_tag ft (); - - (** Get the final string. *) - let output = flush_str_formatter () in - - (** Finalize by restoring the state of the [str_formatter] and the - default behavior of Format. By the way, there may be a bug here: - there is no {!Format.pp_get_tags} and therefore if the tags flags - was already set to true before executing this piece of code, the - state of Format is not restored. *) - set ~spaces:std_spaces; - pp_set_tags ft false; - output - ) - in - (** Second, we retrieve the final function that relates - each tag to an annotation. *) - let get = get_annotations () in - - (** Third, we parse the resulting string. It is a valid XML - document (in the sense of Xml_parser). As blanks are - meaningful we deactivate canonicalization in the XML - parser. *) - let xml_pp = - try - Xml_parser.(parse ~do_not_canonicalize:true (make (SString tagged_pp))) - with Xml_parser.Error e -> - Printf.eprintf - "Broken invariant (RichPp): \n\ - The output semi-structured pretty-printing is ill-formed.\n\ - Please report.\n\ - %s" - (Xml_parser.error e); - exit 1 - in - - (** Fourth, the low-level XML is turned into a high-level - semi-structured document that contains a located annotation in - every node. During the traversal of the low-level XML document, - we build a raw string representation of the pretty-print. *) - let rec node buffer = function - | Element (index, [], cs) -> - let startpos, endpos, cs = children buffer cs in - let annotation = try Some (get index) with _ -> None in - (Element (index, { annotation; startpos; endpos }, cs), endpos) - - | PCData s -> - Buffer.add_string buffer s; - (PCData s, Buffer.length buffer) - - | _ -> - assert false (* Because of the form of XML produced by Format. *) - - and children buffer cs = - let startpos = Buffer.length buffer in - let cs, endpos = - List.fold_left (fun (cs, endpos) c -> - let c, endpos = node buffer c in - (c :: cs, endpos) - ) ([], startpos) cs - in - (startpos, endpos, List.rev cs) - in - let pp_buffer = Buffer.create 13 in - let xml, _ = node pp_buffer xml_pp in - - (** We return the raw pretty-printing and its annotations tree. *) - (Buffer.contents pp_buffer, xml) - -let annotations_positions xml = - let rec node accu = function - | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> - children ((annotation, (startpos, endpos)) :: accu) cs - | Element (_, _, cs) -> - children accu cs - | _ -> - accu - and children accu cs = - List.fold_left node accu cs - in - node [] xml - -let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = - let rec node = function - | Element (index, { annotation; startpos; endpos }, cs) -> - let attributes = - [ "startpos", string_of_int startpos; - "endpos", string_of_int endpos - ] - @ (match annotation with - | None -> [] - | Some annotation -> attributes_of_annotation annotation - ) - in - let tag = - match annotation with - | None -> index - | Some annotation -> tag_of_annotation annotation - in - Element (tag, attributes, List.map node cs) - | PCData s -> - PCData s - in - node xml - - diff --git a/lib/richPp.mli b/lib/richPp.mli deleted file mode 100644 index 834115d40b..0000000000 --- a/lib/richPp.mli +++ /dev/null @@ -1,59 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* index - - (** [get_annotations ()] returns a function to retrieve annotations - from indices after pretty-printing. *) - val get_annotations : unit -> (index -> Annotation.t) - -end - -(** Each annotation of the semi-structured document refers to the - substring it annotates. *) -type 'annotation located = { - annotation : 'annotation option; - startpos : int; - endpos : int -} - -(** [rich_pp get_annotations ppcmds] returns the interpretation - of [ppcmds] as a string as well as a semi-structured document - that represents (located) annotations of this string. *) -val rich_pp : - (unit -> (index -> 'annotation)) -> - (unit -> Pp.std_ppcmds) -> - string * ('annotation located) Xml_datatype.gxml - -(** [annotations_positions ssdoc] returns a list associating each - annotations with its position in the string from which [ssdoc] is - built. *) -val annotations_positions : - 'annotation located Xml_datatype.gxml -> - ('annotation * (int * int)) list - -(** [xml_of_rich_pp ssdoc] returns an XML representation of the - semi-structured document [ssdoc]. *) -val xml_of_rich_pp : - ('annotation -> string) -> - ('annotation -> (string * string) list) -> - 'annotation located Xml_datatype.gxml -> - Xml_datatype.xml - diff --git a/lib/richpp.ml b/lib/richpp.ml new file mode 100644 index 0000000000..f9a7e83a8e --- /dev/null +++ b/lib/richpp.ml @@ -0,0 +1,186 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + incr count; + annotations := annotation :: !annotations; + string_of_int !count + + let get_annotations () = + let annotations = Array.of_list (List.rev !annotations) in + fun index -> annotations.(int_of_string index) + +end + +let rich_pp get_annotations ppcmds = + (** First, we use Format to introduce tags inside + the pretty-printed document. + + Each inserted tag is an index to an annotation. + *) + let tagged_pp = Format.( + + (** Warning: The following instructions are valid only if + [str_formatter] is not used for another purpose in + Pp.pp_with. *) + + let ft = str_formatter in + + (** We reuse {!Format} standard way of producing tags + inside pretty-printing. *) + pp_set_tags ft true; + + (** The whole output must be a valid document. To that + end, we nest the document inside a tag named . *) + pp_open_tag ft "pp"; + + (** XML ignores spaces. The problem is that our pretty-printings + are based on spaces to indent. To solve that problem, we + systematically output non-breakable spaces, which are properly + honored by XML. + + To do so, we reconfigure the [str_formatter] temporarily by + hijacking the function that output spaces. *) + let out, flush, newline, std_spaces = + pp_get_all_formatter_output_functions ft () + in + let set = pp_set_all_formatter_output_functions ft ~out ~flush ~newline in + set ~spaces:(fun k -> + for i = 0 to k - 1 do + Buffer.add_string stdbuf " " + done + ); + + (** Some characters must be escaped in XML. This is done by the + following rewriting of the strings held by pretty-printing + commands. *) + Pp.(pp_with ft (rewrite Xml_printer.pcdata_to_string (ppcmds ()))); + + (** Insert

. *) + pp_close_tag ft (); + + (** Get the final string. *) + let output = flush_str_formatter () in + + (** Finalize by restoring the state of the [str_formatter] and the + default behavior of Format. By the way, there may be a bug here: + there is no {!Format.pp_get_tags} and therefore if the tags flags + was already set to true before executing this piece of code, the + state of Format is not restored. *) + set ~spaces:std_spaces; + pp_set_tags ft false; + output + ) + in + (** Second, we retrieve the final function that relates + each tag to an annotation. *) + let get = get_annotations () in + + (** Third, we parse the resulting string. It is a valid XML + document (in the sense of Xml_parser). As blanks are + meaningful we deactivate canonicalization in the XML + parser. *) + let xml_pp = + try + Xml_parser.(parse ~do_not_canonicalize:true (make (SString tagged_pp))) + with Xml_parser.Error e -> + Printf.eprintf + "Broken invariant (RichPp): \n\ + The output semi-structured pretty-printing is ill-formed.\n\ + Please report.\n\ + %s" + (Xml_parser.error e); + exit 1 + in + + (** Fourth, the low-level XML is turned into a high-level + semi-structured document that contains a located annotation in + every node. During the traversal of the low-level XML document, + we build a raw string representation of the pretty-print. *) + let rec node buffer = function + | Element (index, [], cs) -> + let startpos, endpos, cs = children buffer cs in + let annotation = try Some (get index) with _ -> None in + (Element (index, { annotation; startpos; endpos }, cs), endpos) + + | PCData s -> + Buffer.add_string buffer s; + (PCData s, Buffer.length buffer) + + | _ -> + assert false (* Because of the form of XML produced by Format. *) + + and children buffer cs = + let startpos = Buffer.length buffer in + let cs, endpos = + List.fold_left (fun (cs, endpos) c -> + let c, endpos = node buffer c in + (c :: cs, endpos) + ) ([], startpos) cs + in + (startpos, endpos, List.rev cs) + in + let pp_buffer = Buffer.create 13 in + let xml, _ = node pp_buffer xml_pp in + + (** We return the raw pretty-printing and its annotations tree. *) + (Buffer.contents pp_buffer, xml) + +let annotations_positions xml = + let rec node accu = function + | Element (_, { annotation = Some annotation; startpos; endpos }, cs) -> + children ((annotation, (startpos, endpos)) :: accu) cs + | Element (_, _, cs) -> + children accu cs + | _ -> + accu + and children accu cs = + List.fold_left node accu cs + in + node [] xml + +let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = + let rec node = function + | Element (index, { annotation; startpos; endpos }, cs) -> + let attributes = + [ "startpos", string_of_int startpos; + "endpos", string_of_int endpos + ] + @ (match annotation with + | None -> [] + | Some annotation -> attributes_of_annotation annotation + ) + in + let tag = + match annotation with + | None -> index + | Some annotation -> tag_of_annotation annotation + in + Element (tag, attributes, List.map node cs) + | PCData s -> + PCData s + in + node xml + + diff --git a/lib/richpp.mli b/lib/richpp.mli new file mode 100644 index 0000000000..834115d40b --- /dev/null +++ b/lib/richpp.mli @@ -0,0 +1,59 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* index + + (** [get_annotations ()] returns a function to retrieve annotations + from indices after pretty-printing. *) + val get_annotations : unit -> (index -> Annotation.t) + +end + +(** Each annotation of the semi-structured document refers to the + substring it annotates. *) +type 'annotation located = { + annotation : 'annotation option; + startpos : int; + endpos : int +} + +(** [rich_pp get_annotations ppcmds] returns the interpretation + of [ppcmds] as a string as well as a semi-structured document + that represents (located) annotations of this string. *) +val rich_pp : + (unit -> (index -> 'annotation)) -> + (unit -> Pp.std_ppcmds) -> + string * ('annotation located) Xml_datatype.gxml + +(** [annotations_positions ssdoc] returns a list associating each + annotations with its position in the string from which [ssdoc] is + built. *) +val annotations_positions : + 'annotation located Xml_datatype.gxml -> + ('annotation * (int * int)) list + +(** [xml_of_rich_pp ssdoc] returns an XML representation of the + semi-structured document [ssdoc]. *) +val xml_of_rich_pp : + ('annotation -> string) -> + ('annotation -> (string * string) list) -> + 'annotation located Xml_datatype.gxml -> + Xml_datatype.xml + diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c36ee21eb5..9ee81b278e 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 d2877edc50..5f8b2f7360 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 ad3f95ef24..44f4b456cc 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 36d116f1af..2003cc1e17 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 8814daf70b..21fac8a35c 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 616fc73454..06f51f0607 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 7910702984..652a34fa1f 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 66732319cc..0000000000 --- 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.mli b/printing/richPrinter.mli deleted file mode 100644 index 9d02ad2943..0000000000 --- a/printing/richPrinter.mli +++ /dev/null @@ -1,41 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* rich_pp - -(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) -val richpp_constr : Constrexpr.constr_expr -> rich_pp - -(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *) -val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp diff --git a/printing/richprinter.ml b/printing/richprinter.ml new file mode 100644 index 0000000000..d27b7c3736 --- /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 new file mode 100644 index 0000000000..6df5c9c6a2 --- /dev/null +++ b/printing/richprinter.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* rich_pp + +(** [richpp_constr constr] produces a rich pretty-printing of [constr]. *) +val richpp_constr : Constrexpr.constr_expr -> rich_pp + +(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *) +val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp -- cgit v1.2.3