summaryrefslogtreecommitdiff
path: root/lib/cThread.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/cThread.ml')
-rw-r--r--lib/cThread.ml95
1 files changed, 0 insertions, 95 deletions
diff --git a/lib/cThread.ml b/lib/cThread.ml
deleted file mode 100644
index 4f60a697..00000000
--- a/lib/cThread.ml
+++ /dev/null
@@ -1,95 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-type thread_ic = in_channel
-
-let prepare_in_channel_for_thread_friendly_io ic = ic
-
-let thread_friendly_read_fd fd s ~off ~len =
- let rec loop () =
- try Unix.read fd s off len
- with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
- in
- loop ()
-
-let thread_friendly_read ic s ~off ~len =
- try
- let fd = Unix.descr_of_in_channel ic in
- thread_friendly_read_fd fd s ~off ~len
- with Unix.Unix_error _ -> 0
-
-let really_read_fd fd s off len =
- let i = ref 0 in
- while !i < len do
- let off = off + !i in
- let len = len - !i in
- let r = thread_friendly_read_fd fd s ~off ~len in
- if r = 0 then raise End_of_file;
- i := !i + r
- done
-
-let really_read_fd_2_oc fd oc len =
- let i = ref 0 in
- let size = 4096 in
- let s = String.create size in
- while !i < len do
- let len = len - !i in
- let r = thread_friendly_read_fd fd s ~off:0 ~len:(min len size) in
- if r = 0 then raise End_of_file;
- i := !i + r;
- output oc s 0 r;
- done
-
-let thread_friendly_really_read ic s ~off ~len =
- try
- let fd = Unix.descr_of_in_channel ic in
- really_read_fd fd s off len
- with Unix.Unix_error _ -> raise End_of_file
-
-let thread_friendly_really_read_line ic =
- try
- let fd = Unix.descr_of_in_channel ic in
- let b = Buffer.create 1024 in
- let s = String.make 1 '\000' in
- while s <> "\n" do
- let n = thread_friendly_read_fd fd s ~off:0 ~len:1 in
- if n = 0 then raise End_of_file;
- if s <> "\n" then Buffer.add_string b s;
- done;
- Buffer.contents b
- with Unix.Unix_error _ -> raise End_of_file
-
-let thread_friendly_input_value ic =
- try
- let fd = Unix.descr_of_in_channel ic in
- let header = String.create Marshal.header_size in
- really_read_fd fd header 0 Marshal.header_size;
- let body_size = Marshal.data_size header 0 in
- let desired_size = body_size + Marshal.header_size in
- if desired_size <= Sys.max_string_length then begin
- let msg = String.create desired_size in
- String.blit header 0 msg 0 Marshal.header_size;
- really_read_fd fd msg Marshal.header_size body_size;
- Marshal.from_string msg 0
- end else begin
- (* Workaround for 32 bit systems and data > 16M *)
- let name, oc =
- Filename.open_temp_file ~mode:[Open_binary] "coq" "marshal" in
- try
- output oc header 0 Marshal.header_size;
- really_read_fd_2_oc fd oc body_size;
- close_out oc;
- let ic = open_in_bin name in
- let data = Marshal.from_channel ic in
- close_in ic;
- Sys.remove name;
- data
- with e -> Sys.remove name; raise e
- end
- with Unix.Unix_error _ | Sys_error _ -> raise End_of_file
-