Remove Safe_marshal

Safe_marshal was using intermediate strings that are subject to
Sys.max_string_length limitation. Use directly binary channel-oriented
functions instead. This is a fix for bug #2471. Remark: this might
reduce robustness w.r.t. noise in the communication channel.

AFAIK, the original purpose of Safe_marshal was to work around a bug
on Windows... this should be investigated further.

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

4 files changed, 10 insertions, 51 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 66fcbd059..5db5f0f3a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -122,8 +122,9 @@ let check_connection args =
       exit 1
 
 let eval_call coqtop (c:'a Ide_blob.call) =
-  Safe_marshal.send coqtop.cin c;
-  (Safe_marshal.receive: in_channel -> 'a Ide_blob.value) coqtop.cout
+  Marshal.to_channel coqtop.cin c [];
+  flush coqtop.cin;
+  (Marshal.from_channel: in_channel -> 'a Ide_blob.value) coqtop.cout
 
 let is_in_loadpath coqtop s = eval_call coqtop (Ide_blob.is_in_loadpath s)
  
@@ -143,6 +144,8 @@ let spawn_coqtop sup_args =
   Mutex.lock toplvl_ctr_mtx;
   try 
     let oc,ic = Unix.open_process (coqtop_path ()^" -ideslave "^sup_args) in
+    set_binary_mode_out ic true;
+    set_binary_mode_in oc true;
     incr toplvl_ctr;
     Mutex.unlock toplvl_ctr_mtx;
     { cin = ic; cout = oc ; sup_args = sup_args ; version = 0 }
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 0607ae50e..90b90cb4f 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -23,4 +23,3 @@ Heap
 Option
 Dnet
 Store
-Safe_marshal
diff --git a/lib/safe_marshal.ml b/lib/safe_marshal.ml
deleted file mode 100644
index 4d32245f5..000000000
--- a/lib/safe_marshal.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-(*
-let uuencode s =
-  let norm_s = s ^ (String.make (String.length s mod 3) '\000') in
-  let rec y f x = f (y f) x in
-  let chop rem = function
-    | "" -> []
-    | s -> String.sub s 0 3 :: (rem (String.sub s 3 (String.length (s - 3)))) in
-  let chunks = y chop norm_s in
- *)
-
-let hobcnv = Array.init 256 (fun i -> Printf.sprintf "%.2x" i)
-let bohcnv = Array.init 256 (fun i -> i -
-                                      (if 0x30 <= i then 0x30 else 0) -
-                                      (if 0x41 <= i then 0x7 else 0) -
-                                      (if 0x61 <= i then 0x20 else 0))
-
-let hex_of_bin ch = hobcnv.(int_of_char ch)
-let bin_of_hex s = char_of_int (bohcnv.(int_of_char s.[0]) * 16 + bohcnv.(int_of_char s.[1]))
-
-let send cout expr =
-  let mshl_expr = Marshal.to_string expr [] in
-  let payload = Buffer.create (String.length mshl_expr * 2) in
-  String.iter (fun c -> Buffer.add_string payload (hex_of_bin c)) mshl_expr;
-  Buffer.add_char payload '\n';
-  output_string cout (Buffer.contents payload);
-  flush cout
-
-
-let receive cin =
-  let payload = input_line cin in
-  let mshl_expr_len = String.length payload / 2 in
-  let mshl_expr = Buffer.create mshl_expr_len in
-  let buf = String.create 2 in
-  for i = 0 to mshl_expr_len - 1 do
-    String.blit payload (2*i) buf 0 2;
-    Buffer.add_char mshl_expr (bin_of_hex buf)
-  done;
-  Marshal.from_string (Buffer.contents mshl_expr) 0
-
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml
index 1fd42e419..6ef45a442 100644
--- a/toplevel/ide_blob.ml
+++ b/toplevel/ide_blob.ml
@@ -495,6 +495,8 @@ let init_stdout,read_stdout =
      Pp_control.std_ft := out_ft;
      Pp_control.err_ft := out_ft;
      Pp_control.deep_ft := deep_out_ft;
+     set_binary_mode_out !orig_stdout true;
+     set_binary_mode_in stdin true;
   ),
   (fun () -> Format.pp_print_flush out_ft ();
              let r = Buffer.contents out_buff in
@@ -588,9 +590,10 @@ let contents : Lib.library_segment call =
 let loop () =
   try
     while true do
-      let q = (Safe_marshal.receive: in_channel -> 'a call) stdin in
+      let q = (Marshal.from_channel: in_channel -> 'a call) stdin in
       let r = eval_call q in
-      Safe_marshal.send !orig_stdout r
+      Marshal.to_channel !orig_stdout r [];
+      flush !orig_stdout
     done
   with
     | Vernacexpr.Quit -> exit 0