Commit 852de855 authored by POTTIER Francois's avatar POTTIER Francois

Updated [IO.exhaust].

Modified [PreFront.read_whole_file] to use [IO.exhaust].
parent 92833f0f
......@@ -2,20 +2,21 @@
(* ------------------------------------------------------------------------- *)
(* [exhaust channel] reads all of the data that's available on [channel].
It does not assume that the length of the data is known ahead of time. *)
It does not assume that the length of the data is known ahead of time.
It does not close the channel. *)
let chunk_size =
2048
16384
let exhaust channel =
let buffer = Buffer.create chunk_size in
let chunk = String.create chunk_size in
let chunk = Bytes.create chunk_size in
let rec loop () =
let length = input channel chunk 0 chunk_size in
if length = 0 then
Buffer.contents buffer
else begin
Buffer.add_substring buffer chunk 0 length;
Buffer.add_subbytes buffer chunk 0 length;
loop()
end
in
......
(* Input-output utilities. *)
(* [exhaust channel] reads all of the data that's available on [channel].
It does not assume that the length of the data is known ahead of time.
It does not close the channel. *)
val exhaust: in_channel -> string
(* [invoke command] invokes an external command (which expects no input)
and returns its output, if the command succeeds. It returns [None] if
the command fails. *)
......
......@@ -19,21 +19,9 @@ let read_whole_file filename =
whole file. And the standard library function [Buffer.add_channel] uses
[really_input] internally, so we cannot use it either. Bummer. *)
let block_size = 16384 in
let b = Buffer.create block_size in
let s = Bytes.create block_size in
let rec loop () =
let read = input channel s 0 block_size in
if read > 0 then begin
Buffer.add_subbytes b s 0 read;
loop()
end
in
loop();
let s = IO.exhaust channel in
close_in channel;
Buffer.contents b
s
let load_partial_grammar filename =
let validExt = if Settings.coq then ".vy" else ".mly" in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment