| changeset 75569 | f848f66a8cb7 |
| parent 73559 | 22b5ecb53dd9 |
| child 75571 | ac5e633ad9b3 |
--- 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