New module Xml_printer (dual to Xml_parser)

Code for printing XML moved from xml_utils.ml to xml_printer.ml
and improved to generate less garbage using Buffer.t systematically.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 156 insertions, 154 deletions

diff --git a/lib/lib.mllib b/lib/lib.mllib
index eabac2cfd8..0ff2d97e95 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,5 +1,6 @@
 Xml_lexer
 Xml_parser
+Xml_printer
 Errors
 Bigint
 Dyn
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
new file mode 100644
index 0000000000..ae4d34c773
--- /dev/null
+++ b/lib/xml_printer.ml
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type xml = Serialize.xml =
+        | Element of (string * (string * string) list * xml list)
+        | PCData of string
+
+type target = TChannel of out_channel | TBuffer of Buffer.t
+
+type t = target
+
+let make x = x
+
+let buffer_pcdata tmp text =
+	let l = String.length text in
+	for p = 0 to l-1 do 
+		match text.[p] with
+		| '>' -> Buffer.add_string tmp "&gt;"
+		| '<' -> Buffer.add_string tmp "&lt;"
+		| '&' ->
+			if p < l-1 && text.[p+1] = '#' then
+				Buffer.add_char tmp '&'
+			else
+				Buffer.add_string tmp "&amp;"
+		| '\'' -> Buffer.add_string tmp "&apos;"
+		| '"' -> Buffer.add_string tmp "&quot;"
+		| c -> Buffer.add_char tmp c
+	done
+
+let buffer_attr tmp (n,v) =
+	Buffer.add_char tmp ' ';
+	Buffer.add_string tmp n;
+	Buffer.add_string tmp "=\"";
+	let l = String.length v in
+	for p = 0 to l-1 do
+		match v.[p] with
+		| '\\' -> Buffer.add_string tmp "\\\\"
+		| '"' -> Buffer.add_string tmp "\\\""
+		| c -> Buffer.add_char tmp c
+	done;
+	Buffer.add_char tmp '"'
+
+let to_buffer tmp x = 
+	let pcdata = ref false in
+	let rec loop = function
+		| Element (tag,alist,[]) ->
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter (buffer_attr tmp) alist;
+			Buffer.add_string tmp "/>";
+			pcdata := false;
+		| Element (tag,alist,l) ->
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter (buffer_attr tmp) alist;
+			Buffer.add_char tmp '>';
+			pcdata := false;
+			List.iter loop l;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			pcdata := false;
+		| PCData text ->
+			if !pcdata then Buffer.add_char tmp ' ';
+			buffer_pcdata tmp text;
+			pcdata := true;
+	in
+	loop x
+
+let to_string x =
+  let b = Buffer.create 200 in
+  to_buffer b x;
+  Buffer.contents b
+
+let to_string_fmt x =
+        let tmp = Buffer.create 200 in
+	let rec loop ?(newl=false) tab = function
+		| Element (tag,alist,[]) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter (buffer_attr tmp) alist;
+			Buffer.add_string tmp "/>";
+			if newl then Buffer.add_char tmp '\n';
+		| Element (tag,alist,[PCData text]) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter (buffer_attr tmp) alist;
+			Buffer.add_string tmp ">";
+			buffer_pcdata tmp text;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			if newl then Buffer.add_char tmp '\n';
+		| Element (tag,alist,l) ->
+			Buffer.add_string tmp tab;
+			Buffer.add_char tmp '<';
+			Buffer.add_string tmp tag;
+			List.iter (buffer_attr tmp) alist;
+			Buffer.add_string tmp ">\n";
+			List.iter (loop ~newl:true (tab^"  ")) l;
+			Buffer.add_string tmp tab;
+			Buffer.add_string tmp "</";
+			Buffer.add_string tmp tag;
+			Buffer.add_char tmp '>';
+			if newl then Buffer.add_char tmp '\n';
+		| PCData text ->
+			buffer_pcdata tmp text;
+			if newl then Buffer.add_char tmp '\n';
+	in
+	loop "" x;
+	Buffer.contents tmp
+
+let print t xml =
+  let tmp, flush = match t with
+    | TChannel oc ->
+        let b = Buffer.create 200 in
+        b, (fun () -> Buffer.output_buffer oc b; flush oc)
+    | TBuffer b -> b, (fun () -> ()) in
+  to_buffer tmp xml;
+  flush ()
+;;
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
new file mode 100644
index 0000000000..b19e189432
--- /dev/null
+++ b/lib/xml_printer.mli
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type xml = Serialize.xml
+
+type t
+type target = TChannel of out_channel | TBuffer of Buffer.t
+
+val make : target -> t
+
+(** Print the xml data structure to a source into a compact xml string (without
+ any user-readable formating ). *)
+val print : t -> xml -> unit
+
+(** Print the xml data structure into a compact xml string (without
+ any user-readable formating ). *)
+val to_string : xml -> string
+
+(** Print the xml data structure into an user-readable string with
+ tabs and lines break between different nodes. *)
+val to_string_fmt : xml -> string
+
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
index 60efab577f..53e694c7a0 100644
--- a/lib/xml_utils.ml
+++ b/lib/xml_utils.ml
@@ -68,144 +68,3 @@ let fold f v = function
 	| Element (_,_,clist) -> List.fold_left f v clist
 	| x -> raise (Not_element x)
 
-let tmp = Buffer.create 200
-
-let buffer_pcdata text =
-	let l = String.length text in
-	for p = 0 to l-1 do 
-		match text.[p] with
-		| '>' -> Buffer.add_string tmp "&gt;"
-		| '<' -> Buffer.add_string tmp "&lt;"
-		| '&' ->
-			if p < l-1 && text.[p+1] = '#' then
-				Buffer.add_char tmp '&'
-			else
-				Buffer.add_string tmp "&amp;"
-		| '\'' -> Buffer.add_string tmp "&apos;"
-		| '"' -> Buffer.add_string tmp "&quot;"
-		| c -> Buffer.add_char tmp c
-	done
-
-let print_pcdata chan text =
-  let l = String.length text in
-  for p = 0 to l-1 do 
-    match text.[p] with
-    | '>' -> Printf.fprintf chan "&gt;"
-    | '<' -> Printf.fprintf chan "&lt;"
-    | '&' ->
-            if p < l-1 && text.[p+1] = '#' then
-                    Printf.fprintf chan "&"
-            else
-                    Printf.fprintf chan "&amp;"
-    | '\'' -> Printf.fprintf chan "&apos;"
-    | '"' -> Printf.fprintf chan "&quot;"
-    | c -> Printf.fprintf chan "%c" c
-  done
-
-let buffer_attr (n,v) =
-	Buffer.add_char tmp ' ';
-	Buffer.add_string tmp n;
-	Buffer.add_string tmp "=\"";
-	let l = String.length v in
-	for p = 0 to l-1 do
-		match v.[p] with
-		| '\\' -> Buffer.add_string tmp "\\\\"
-		| '"' -> Buffer.add_string tmp "\\\""
-		| c -> Buffer.add_char tmp c
-	done;
-	Buffer.add_char tmp '"'
-
-let print_attr chan (n, v) =
-  Printf.fprintf chan " %s=\"" n;
-  let l = String.length v in
-  for p = 0 to l-1 do
-          match v.[p] with
-          | '\\' -> Printf.fprintf chan "\\\\"
-          | '"' -> Printf.fprintf chan  "\\\""
-          | c -> Printf.fprintf chan "%c" c
-  done;
-  Printf.fprintf chan "\""
-
-let print_attrs chan l = List.iter (print_attr chan) l
-
-let rec print_xml chan = function
-| Element (tag, alist, []) ->
-  Printf.fprintf chan "<%s%a/>" tag print_attrs alist;
-| Element (tag, alist, l) ->
-  Printf.fprintf chan "<%s%a>%a</%s>" tag print_attrs alist
-  (fun chan -> List.iter (print_xml chan)) l tag
-| PCData text ->
-  print_pcdata chan text
-
-let to_string x = 
-	let pcdata = ref false in
-	let rec loop = function
-		| Element (tag,alist,[]) ->
-			Buffer.add_char tmp '<';
-			Buffer.add_string tmp tag;
-			List.iter buffer_attr alist;
-			Buffer.add_string tmp "/>";
-			pcdata := false;
-		| Element (tag,alist,l) ->
-			Buffer.add_char tmp '<';
-			Buffer.add_string tmp tag;
-			List.iter buffer_attr alist;
-			Buffer.add_char tmp '>';
-			pcdata := false;
-			List.iter loop l;
-			Buffer.add_string tmp "</";
-			Buffer.add_string tmp tag;
-			Buffer.add_char tmp '>';
-			pcdata := false;
-		| PCData text ->
-			if !pcdata then Buffer.add_char tmp ' ';
-			buffer_pcdata text;
-			pcdata := true;
-	in
-	Buffer.reset tmp;
-	loop x;
-	let s = Buffer.contents tmp in
-	Buffer.reset tmp;
-	s
-
-let to_string_fmt x =
-	let rec loop ?(newl=false) tab = function
-		| Element (tag,alist,[]) ->
-			Buffer.add_string tmp tab;
-			Buffer.add_char tmp '<';
-			Buffer.add_string tmp tag;
-			List.iter buffer_attr alist;
-			Buffer.add_string tmp "/>";
-			if newl then Buffer.add_char tmp '\n';
-		| Element (tag,alist,[PCData text]) ->
-			Buffer.add_string tmp tab;
-			Buffer.add_char tmp '<';
-			Buffer.add_string tmp tag;
-			List.iter buffer_attr alist;
-			Buffer.add_string tmp ">";
-			buffer_pcdata text;
-			Buffer.add_string tmp "</";
-			Buffer.add_string tmp tag;
-			Buffer.add_char tmp '>';
-			if newl then Buffer.add_char tmp '\n';
-		| Element (tag,alist,l) ->
-			Buffer.add_string tmp tab;
-			Buffer.add_char tmp '<';
-			Buffer.add_string tmp tag;
-			List.iter buffer_attr alist;
-			Buffer.add_string tmp ">\n";
-			List.iter (loop ~newl:true (tab^"  ")) l;
-			Buffer.add_string tmp tab;
-			Buffer.add_string tmp "</";
-			Buffer.add_string tmp tag;
-			Buffer.add_char tmp '>';
-			if newl then Buffer.add_char tmp '\n';
-		| PCData text ->
-			buffer_pcdata text;
-			if newl then Buffer.add_char tmp '\n';
-	in
-	Buffer.reset tmp;
-	loop "" x;
-	let s = Buffer.contents tmp in
-	Buffer.reset tmp;
-	s
diff --git a/lib/xml_utils.mli b/lib/xml_utils.mli
index 56e7f80762..67cd5cb93a 100644
--- a/lib/xml_utils.mli
+++ b/lib/xml_utils.mli
@@ -78,16 +78,3 @@ val map : (xml -> 'a) -> xml -> 'a list
  Raise {!Xml.Not_element} if the xml is not an element *)
 val fold : ('a -> xml -> 'a) -> 'a -> xml -> 'a
 
-(** {6 Xml Printing} *)
-
-(** Print the xml data structure to a channel into a compact xml string (without
- any user-readable formating ). *)
-val print_xml : out_channel -> xml -> unit
-
-(** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
-val to_string : xml -> string
-
-(** Print the xml data structure into an user-readable string with
- tabs and lines break between different nodes. *)
-val to_string_fmt : xml -> string