author | wenzelm |
Sun, 16 Jun 2024 11:55:25 +0200 | |
changeset 80386 | 10f47bb1abd3 |
parent 80385 | 605e19319343 |
child 80387 | afaac8c6048e |
--- a/src/Pure/PIDE/byte_message.scala Sun Jun 16 11:50:42 2024 +0200 +++ b/src/Pure/PIDE/byte_message.scala Sun Jun 16 11:55:25 2024 +0200 @@ -90,8 +90,9 @@ } def write_line_message(stream: OutputStream, msg: Bytes): Unit = { - if (is_length(msg) || is_terminated(msg)) + if (is_length(msg) || is_terminated(msg)) { error ("Bad content for line message:\n" ++ msg.text.take(100)) + } val n = msg.size write(stream,