tuned;
authorwenzelm
Thu Feb 28 21:16:17 2019 +0100 (7 weeks ago ago)
changeset 70029bf2cd27714fb
parent 70028 a12d2eb58aca
child 70030 09f200c658ed
tuned;
src/Pure/PIDE/byte_message.ML
     1.1 --- a/src/Pure/PIDE/byte_message.ML	Wed Feb 27 22:08:07 2019 +0100
     1.2 +++ b/src/Pure/PIDE/byte_message.ML	Thu Feb 28 21:16:17 2019 +0100
     1.3 @@ -55,11 +55,11 @@
     1.4  
     1.5  (* messages with multiple chunks (arbitrary content) *)
     1.6  
     1.7 -fun make_header stream ns =
     1.8 +fun make_header ns =
     1.9    [space_implode "," (map Value.print_int ns), "\n"];
    1.10  
    1.11  fun write_message stream chunks =
    1.12 -  (write stream (make_header stream (map size chunks) @ chunks); flush stream);
    1.13 +  (write stream (make_header (map size chunks) @ chunks); flush stream);
    1.14  
    1.15  fun parse_header line =
    1.16    map Value.parse_nat (space_explode "," line)
    1.17 @@ -92,7 +92,7 @@
    1.18      let val n = size msg in
    1.19        write stream
    1.20          ((if n > 100 orelse exists_string (fn s => s = "\n") msg
    1.21 -          then make_header stream [n + 1] else []) @ [msg, "\n"]);
    1.22 +          then make_header [n + 1] else []) @ [msg, "\n"]);
    1.23        flush stream
    1.24      end;
    1.25