--- a/src/Pure/PIDE/byte_message.ML Wed Feb 27 22:08:07 2019 +0100
+++ b/src/Pure/PIDE/byte_message.ML Thu Feb 28 21:16:17 2019 +0100
@@ -55,11 +55,11 @@
(* messages with multiple chunks (arbitrary content) *)
-fun make_header stream ns =
+fun make_header ns =
[space_implode "," (map Value.print_int ns), "\n"];
fun write_message stream chunks =
- (write stream (make_header stream (map size chunks) @ chunks); flush stream);
+ (write stream (make_header (map size chunks) @ chunks); flush stream);
fun parse_header line =
map Value.parse_nat (space_explode "," line)
@@ -92,7 +92,7 @@
let val n = size msg in
write stream
((if n > 100 orelse exists_string (fn s => s = "\n") msg
- then make_header stream [n + 1] else []) @ [msg, "\n"]);
+ then make_header [n + 1] else []) @ [msg, "\n"]);
flush stream
end;