diff options
author | Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-05 20:51:16 +0100 |
---|---|---|
committer | Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-05 20:51:16 +0100 |
commit | 3d2b9f1329557dd54720718bf064010d9538ea03 (patch) | |
tree | da0c8df97286e982d8d7e79624344388b1c85760 | |
parent | c442153f1af0823a95c6b6c31243e43a0f336ee6 (diff) |
lib/richPp: Fix a bug related to the compatibility with ocaml 3.12
- The previous version of this module was using a feature of
the Format module of ocaml 4.01.
- Add comments.
-rw-r--r-- | lib/richPp.ml | 48 |
1 files changed, 40 insertions, 8 deletions
diff --git a/lib/richPp.ml b/lib/richPp.ml index a0039f918..f9a7e83a8 100644 --- a/lib/richPp.ml +++ b/lib/richPp.ml @@ -40,23 +40,55 @@ let rich_pp get_annotations ppcmds = 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>. *) pp_open_tag ft "pp"; - let fof = pp_get_formatter_out_functions ft () in - pp_set_formatter_out_functions ft { fof with - out_spaces = fun k -> - for i = 0 to k - 1 do - Buffer.add_string stdbuf " " - done - }; + + (** 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 </p>. *) pp_close_tag ft (); + + (** Get the final string. *) let output = flush_str_formatter () in - pp_set_formatter_out_functions ft fof; + + (** 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 ) |