Removing dead code relative to the XML plugin.

4 files changed, 0 insertions, 58 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 790acfef5..5d8cdc30f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -76,8 +76,6 @@ let profile = false
 
 let print_emacs = ref false
 
-let xml_export = ref false
-
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 11909c5fa..5dba938b5 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -37,8 +37,6 @@ val profile : bool
 
 val print_emacs : bool ref
 
-val xml_export : bool ref
-
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
diff --git a/lib/system.ml b/lib/system.ml
index 59260fbf6..511b84ab4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -209,56 +209,6 @@ let with_magic_number_check f a =
     (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++
     strbrk "It is corrupted or was compiled with another version of Coq.")
 
-(* Communication through files with another executable *)
-
-let connect writefun readfun com =
-  (* step 0 : prepare temporary files and I/O channels *)
-  let name = Filename.basename com in
-  let req,req_wr =
-    try Filename.open_temp_file ("coq-"^name^"-in") ".xml"
-    with Sys_error s -> error ("Cannot set connection to "^com^"("^s^")") in
-  let ans,ans_wr =
-    try Filename.open_temp_file ("coq-"^name^"-out") ".xml"
-    with Sys_error s ->
-      close_out req_wr;
-      error ("Cannot set connection from "^com^"("^s^")") in
-  let ans_wr' = Unix.descr_of_out_channel ans_wr in
-  (* step 1 : fill the request file *)
-  writefun req_wr;
-  close_out req_wr;
-  (* step 2a : prepare the request-reading descriptor for the sub-process *)
-  let req_rd' =
-    try Unix.openfile req [Unix.O_RDONLY] 0o644
-    with Unix.Unix_error (err,_,_) ->
-      close_out ans_wr;
-      let msg = Unix.error_message err in
-      error ("Cannot set connection to "^com^"("^msg^")")
-  in
-  (* step 2b : launch the sub-process *)
-  let pid =
-    try Unix.create_process com [|com|] req_rd' ans_wr' Unix.stdout
-    with Unix.Unix_error (err,_,_) ->
-      Unix.close req_rd'; close_out ans_wr; Unix.unlink req; Unix.unlink ans;
-      let msg = Unix.error_message err in
-      error ("Cannot execute "^com^"("^msg^")") in
-  Unix.close req_rd';
-  close_out ans_wr;
-  (* step 2c : wait for termination of the sub-process *)
-  (match CUnix.waitpid_non_intr pid with
-    | Unix.WEXITED 127 -> error (com^": cannot execute")
-    | Unix.WEXITED 0 -> ()
-    | _ -> error (com^" exited abnormally"));
-  (* step 3 : read the answer and handle it *)
-  let ans_rd =
-    try open_in ans
-    with Sys_error s -> error ("Cannot read output of "^com^"("^s^")") in
-  let a = readfun ans_rd in
-  close_in ans_rd;
-  (* step 4 : cleanup the temporary files *)
-  unlink req;
-  unlink ans;
-  a
-
 (* Time stamps. *)
 
 type time = float * float * float
diff --git a/lib/system.mli b/lib/system.mli
index 0569c7889..af797121a 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -56,10 +56,6 @@ val marshal_out_segment : string -> out_channel -> 'a -> unit
 val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
 val skip_in_segment : string -> in_channel -> int * Digest.t
 
-(** {6 Sending/receiving once with external executable } *)
-
-val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
-
 (** {6 Time stamps.} *)
 
 type time