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 ++++++++++++++++++ 5 files changed, 246 insertions(+), 246 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 (limited to 'lib') 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 + -- cgit v1.2.3