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

1 files changed, 5 insertions, 2 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 }