diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 11:48:50 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 11:48:50 +0000 |
commit | eed2bb82eb4b97881f155079fd457a8de75bdba5 (patch) | |
tree | bdad1789ce20b86b58f2414ac7b80cbd959ea7c3 /lib | |
parent | 12c796fe185876021e2dfc7753b8f90ba9de31e0 (diff) |
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
Diffstat (limited to 'lib')
-rw-r--r-- | lib/lib.mllib | 1 | ||||
-rw-r--r-- | lib/safe_marshal.ml | 46 |
2 files changed, 0 insertions, 47 deletions
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 - |