Also sprach CoqIDE (in XML)

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

3 files changed, 25 insertions, 7 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f635ad4073..93eac0962e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -199,10 +199,14 @@ let kill_coqtop coqtop =
 
 (** Cf [Ide_intf] for more details *)
 
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
 let eval_call coqtop (c:'a Ide_intf.call) =
-  Marshal.to_channel coqtop.cin c [];
+  Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
   flush coqtop.cin;
-  (Marshal.from_channel: in_channel -> 'a Ide_intf.value) coqtop.cout
+  let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
+  (Ide_intf.to_answer xml : 'a Ide_intf.value)
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
   eval_call coqtop (Ide_intf.interp (raw,verbose,s))
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 50e56d8468..6ae5f7ea70 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -12,10 +12,16 @@ exception Comment
 
 let coqtop = ref (stdin, stdout)
 
+let p = Xml_parser.make ()
+let () = Xml_parser.check_eof p false
+
 let eval_call (call:'a Ide_intf.call) =
   prerr_endline (Ide_intf.pr_call call);
-  Marshal.to_channel (snd !coqtop) call []; flush (snd !coqtop);
-  let res = ((Marshal.from_channel (fst !coqtop)) : 'a Ide_intf.value) in
+  let xml_query = Ide_intf.of_call call in
+  Xml_utils.print_xml (snd !coqtop) xml_query;
+  flush (snd !coqtop);
+  let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
+  let res = Ide_intf.to_answer xml_answer in
   prerr_endline (Ide_intf.pr_full_value call res);
   match res with Ide_intf.Fail _ -> exit 1 | _ -> ()
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index a9bab94652..cbd7d43537 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -518,6 +518,8 @@ let pr_debug s =
   if !Flags.debug then Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
 
 let loop () =
+  let p = Xml_parser.make () in
+  let () = Xml_parser.check_eof p false in
   init_signal_handler ();
   catch_break := false;
   (* ensure we have a command separator object (DOT) so that the first
@@ -525,15 +527,21 @@ let loop () =
   Lib.mark_end_of_command();
   try
     while true do
-      let q = (Marshal.from_channel: in_channel -> 'a Ide_intf.call) stdin in
+      let xml_query = Xml_parser.parse p (Xml_parser.SChannel stdin) in
+      let q = Ide_intf.to_call xml_query in
       pr_debug ("<-- " ^ Ide_intf.pr_call q);
       let r = eval_call q in
       pr_debug ("--> " ^ Ide_intf.pr_full_value q r);
-      Marshal.to_channel !orig_stdout r []; flush !orig_stdout
+      let xml_answer = Ide_intf.of_answer q r in
+      Xml_utils.print_xml !orig_stdout xml_answer;
+      flush !orig_stdout
     done
   with e ->
     let msg = Printexc.to_string e in
     let r = Ide_intf.Fail (None, "Fatal exception in coqtop:\n" ^ msg) in
     pr_debug ("==> " ^ Ide_intf.pr_value r);
-    (try Marshal.to_channel !orig_stdout r []; flush !orig_stdout with _ -> ());
+    (try
+      Xml_utils.print_xml !orig_stdout (Ide_intf.of_value (fun _ -> assert false) r);
+      flush !orig_stdout
+    with _ -> ());
     exit 1