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

10 files changed, 196 insertions, 186 deletions

diff --git a/Makefile.build b/Makefile.build
index 80ff59f71..b68a02cf6 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -541,7 +541,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ)))
 # fake_ide : for debugging or test-suite purpose, a fake ide simulating
 # a connection to coqtop -ideslave
 
-$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) tools/fake_ide$(BESTOBJ)
+$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) tools/fake_ide$(BESTOBJ)
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml,,unix)
 
diff --git a/Makefile.common b/Makefile.common
index 1934fd493..8aaf8fceb 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -208,7 +208,7 @@ endif
 LINKCMO:=$(CORECMA) $(STATICPLUGINS)
 LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa)
 
-IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo
+IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo
 IDECMA:=ide/ide.cma
 
 LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml
diff --git a/ide/coq.ml b/ide/coq.ml
index 9b08b4f10..9987ed210 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -249,10 +249,12 @@ let _ = Glib.Timeout.add ~ms:300 ~callback:check_zombies
 
 type handle = {
   pid : unix_process_id;
-  cout : Unix.file_descr;
-  cin : out_channel;
   mutable alive : bool;
   mutable waiting_for : (ccb * logger) option; (* last call + callback + log *)
+  xml_oc : Xml_printer.t;
+  xml_ic : Xml_parser.t;
+  glib_ic : Glib.Io.channel;
+  close_xml_channels : unit -> unit
 }
 
 (** Coqtop process status :
@@ -336,7 +338,11 @@ let open_process_pid prog args =
   Unix.close ide2top_r;
   Unix.close top2ide_w;
   Unix.set_nonblock top2ide_r;
-  (pid,top2ide_r,Unix.out_channel_of_descr ide2top_w)
+  pid, 
+  Unix.in_channel_of_descr top2ide_r, 
+  Glib.Io.channel_of_descr top2ide_r,
+  Unix.out_channel_of_descr ide2top_w,
+  (fun () -> Unix.close top2ide_r; Unix.close ide2top_w)
 
 exception TubeError
 exception AnswerWithoutRequest
@@ -378,7 +384,7 @@ type input_state = {
 }
 
 let unsafe_handle_input handle feedback_processor state conds =
-  let chan = Glib.Io.channel_of_descr handle.cout in
+  let chan = handle.glib_ic in
   let () = check_errors conds in
   let s = io_read_all chan in
   let () = if String.length s = 0 then raise TubeError in
@@ -427,7 +433,7 @@ let unsafe_handle_input handle feedback_processor state conds =
     ()
 
 let install_input_watch handle respawner feedback_processor =
-  let io_chan = Glib.Io.channel_of_descr handle.cout in
+  let io_chan = handle.glib_ic in
   let all_conds = [`ERR; `HUP; `IN; `NVAL; `PRI] in (* all except `OUT *)
   let state = {
     fragment = "";
@@ -455,13 +461,18 @@ let install_input_watch handle respawner feedback_processor =
 let spawn_handle args =
   let prog = coqtop_path () in
   let args = Array.of_list (prog :: "-ideslave" :: args) in
-  let (pid, in_fd, oc) = open_process_pid prog args in
+  let pid, ic, gic, oc, close_channels = open_process_pid prog args in
+  let xml_ic = Xml_parser.make (Xml_parser.SChannel ic) in
+  let xml_oc = Xml_printer.make (Xml_printer.TChannel oc) in
+  Xml_parser.check_eof xml_ic false;
   {
     pid = pid;
-    cin = oc;
-    cout = in_fd;
     alive = true;
     waiting_for = None;
+    xml_oc = xml_oc;
+    xml_ic = xml_ic;
+    glib_ic = gic;
+    close_xml_channels = close_channels
   }
 
 (** This clears any potentially remaining open garbage. *)
@@ -469,8 +480,7 @@ let clear_handle h =
   if h.alive then begin
     (* invalidate the old handle *)
     h.alive <- false;
-    ignore_error close_out h.cin;
-    ignore_error Unix.close h.cout;
+    h.close_xml_channels ();
     (* we monitor the death of the old process *)
     zombies := (h.pid,0) :: !zombies
   end
@@ -554,8 +564,7 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log ("Start eval_call " ^ Serialize.pr_call call);
   assert (handle.alive && handle.waiting_for = None);
   handle.waiting_for <- Some (mk_ccb (call,k), logger);
-  Xml_utils.print_xml handle.cin (Serialize.of_call call);
-  flush handle.cin;
+  Xml_printer.print handle.xml_oc (Serialize.of_call call);
   Minilib.log "End eval_call";
   Void
 
diff --git a/lib/lib.mllib b/lib/lib.mllib
index eabac2cfd..0ff2d97e9 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 000000000..ae4d34c77
--- /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 000000000..b19e18943
--- /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 60efab577..53e694c7a 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 56e7f8076..67cd5cb93 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
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 6a4823ee0..5dcefcd88 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,7 +12,7 @@ exception Comment
 
 type coqtop = {
   in_chan : in_channel;
-  out_chan : out_channel;
+  xml_printer : Xml_printer.t;
   xml_parser : Xml_parser.t;
 }
 
@@ -21,8 +21,7 @@ let logger level content = ()
 let eval_call call coqtop =
   prerr_endline (Serialize.pr_call call);
   let xml_query = Serialize.of_call call in
-  Xml_utils.print_xml coqtop.out_chan xml_query;
-  flush coqtop.out_chan;
+  Xml_printer.print coqtop.xml_printer xml_query;
   let rec loop () =
     let xml = Xml_parser.parse coqtop.xml_parser in
     if Serialize.is_message xml then
@@ -88,11 +87,12 @@ let main =
   in
   let coqtop =
     let (cin, cout) = Unix.open_process (coqtop_name^" -ideslave") in
-    let p = Xml_parser.make (Xml_parser.SChannel cin) in
+    let ip = Xml_parser.make (Xml_parser.SChannel cin) in
+    let op = Xml_printer.make (Xml_printer.TChannel cout) in
     {
       in_chan = cin;
-      out_chan = cout;
-      xml_parser = p;
+      xml_printer = op;
+      xml_parser = ip;
     }
   in
   while true do
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 7a826c1da..709062f1f 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -327,7 +327,7 @@ let eval_call c =
 
 (** Message dispatching. *)
 
-let slave_logger level message =
+let slave_logger xml_oc level message =
   (* convert the message into XML *)
   let msg = Pp.string_of_ppcmds (hov 0 message) in
   let message = {
@@ -335,14 +335,11 @@ let slave_logger level message =
     Interface.message_content = msg;
   } in
   let xml = Serialize.of_message message in
-  (* Send it to stdout *)
-  Xml_utils.print_xml !orig_stdout xml;
-  flush !orig_stdout
+  Xml_printer.print xml_oc xml
 
-let slave_feeder msg =
+let slave_feeder xml_oc msg =
   let xml = Serialize.of_feedback msg in
-  Xml_utils.print_xml !orig_stdout xml;
-  flush !orig_stdout
+  Xml_printer.print xml_oc xml
 
 (** The main loop *)
 
@@ -353,21 +350,23 @@ let slave_feeder msg =
 let loop () =
   init_signal_handler ();
   catch_break := false;
-  Pp.set_logger slave_logger;
-  Pp.set_feeder slave_feeder;
+  let xml_oc = Xml_printer.make (Xml_printer.TChannel !orig_stdout) in
+  let xml_ic = Xml_parser.make (Xml_parser.SChannel stdin) in
+  let () = Xml_parser.check_eof xml_ic false in
+  Pp.set_logger (slave_logger xml_oc);
+  Pp.set_feeder (slave_feeder xml_oc);
   (* We'll handle goal fetching and display in our own way *)
   Vernacentries.enable_goal_printing := false;
   Vernacentries.qed_display_script := false;
   Flags.make_term_color false;
   while not !quit do
     try
-      let p = Xml_parser.make (Xml_parser.SChannel stdin) in
-      let xml_query = Xml_parser.parse p in
+      let xml_query = Xml_parser.parse xml_ic in
       let q = Serialize.to_call xml_query in
       let () = pr_debug_call q in
       let r = eval_call q in
       let () = pr_debug_answer q r in
-      Xml_utils.print_xml !orig_stdout (Serialize.of_answer q r);
+      Xml_printer.print xml_oc (Serialize.of_answer q r);
       flush !orig_stdout
     with
       | Xml_parser.Error (Xml_parser.Empty, _) ->