# HG changeset patch
# User wenzelm
# Date 1655814154 -7200
# Node ID f848f66a8cb7b352590be743958b0a140a1a4813
# Parent  a8539b1c8775136090b52068a0896fa97be21329
tuned signature;

diff -r a8539b1c8775 -r f848f66a8cb7 src/Pure/General/bytes.ML
--- 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);
diff -r a8539b1c8775 -r f848f66a8cb7 src/Pure/General/file.ML
--- 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 *)
diff -r a8539b1c8775 -r f848f66a8cb7 src/Pure/PIDE/byte_message.ML
--- 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