--- a/src/Pure/General/bytes.ML Tue Jun 21 14:08:02 2022 +0200
+++ b/src/Pure/General/bytes.ML Tue Jun 21 14:22:34 2022 +0200
@@ -70,13 +70,10 @@
val buffer = build o fold add o Buffer.contents;
-fun read_chunk stream =
- Byte.bytesToString (BinIO.inputN (stream, chunk_size));
-
val read = File.open_input (fn stream =>
let
fun read_bytes bytes =
- (case read_chunk stream of
+ (case File.input_size chunk_size stream of
"" => bytes
| s => read_bytes (add s bytes))
in read_bytes empty end);
--- a/src/Pure/General/file.ML Tue Jun 21 14:08:02 2022 +0200
+++ b/src/Pure/General/file.ML Tue Jun 21 14:22:34 2022 +0200
@@ -26,6 +26,9 @@
val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val read_dir: Path.T -> string list
+ val input: BinIO.instream -> string
+ val input_size: int -> BinIO.instream -> string
+ val input_all: BinIO.instream -> string
val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
val read_lines: Path.T -> string list
@@ -130,6 +133,10 @@
(* input *)
+val input = Byte.bytesToString o BinIO.input;
+fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
+val input_all = Byte.bytesToString o BinIO.inputAll;
+
(*
scalable iterator:
. avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
@@ -138,7 +145,7 @@
fun fold_chunks terminator f path a = open_input (fn file =>
let
fun read buf x =
- (case Byte.bytesToString (BinIO.input file) of
+ (case input file of
"" => (case Buffer.content buf of "" => x | line => f line x)
| input =>
(case String.fields (fn c => c = terminator) input of
@@ -154,7 +161,7 @@
fun read_lines path = rev (fold_lines cons path []);
fun read_pages path = rev (fold_pages cons path []);
-val read = open_input (Byte.bytesToString o BinIO.inputAll);
+val read = open_input input_all;
(* output *)
--- a/src/Pure/PIDE/byte_message.ML Tue Jun 21 14:08:02 2022 +0200
+++ b/src/Pure/PIDE/byte_message.ML Tue Jun 21 14:22:34 2022 +0200
@@ -36,7 +36,7 @@
(* input operations *)
-fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
+fun read stream n = File.input_size n stream;
fun read_block stream n =
let