tuned;
authorwenzelm
Sun, 16 Jun 2024 11:55:25 +0200
changeset 80386 10f47bb1abd3
parent 80385 605e19319343
child 80387 afaac8c6048e
tuned;
src/Pure/PIDE/byte_message.scala
--- 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,