# HG changeset patch
# User wenzelm
# Date 1551384977 -3600
# Node ID bf2cd27714fb4899f3a6f7a158c2aac1408e8824
# Parent  a12d2eb58aca330711b9f37208c56ccefaeb6d75
tuned;

diff -r a12d2eb58aca -r bf2cd27714fb src/Pure/PIDE/byte_message.ML
--- 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;