From eed2bb82eb4b97881f155079fd457a8de75bdba5 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 6 Jan 2011 11:48:50 +0000 Subject: 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 --- toplevel/ide_blob.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'toplevel/ide_blob.ml') 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 -- cgit v1.2.3