# HG changeset patch
# User wenzelm
# Date 1718554735 -7200
# Node ID c22a56495b4c4c0df3dd3a1ead00050afea0136d
# Parent  439ec9b69b6c402f7c0051e7bb88186165d2a844
tuned: prefer Bytes operations;

diff -r 439ec9b69b6c -r c22a56495b4c src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Sun Jun 16 18:17:54 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Sun Jun 16 18:18:55 2024 +0200
@@ -6,7 +6,7 @@
 
 package isabelle
 
-import java.io.{ByteArrayOutputStream, OutputStream, InputStream, IOException}
+import java.io.{OutputStream, InputStream, IOException}
 
 
 object Byte_Message {
@@ -37,17 +37,14 @@
   }
 
   def read_line(stream: InputStream): Option[Bytes] = {
-    val line = new ByteArrayOutputStream(100)
     var c = 0
-    while ({ c = stream.read; c != -1 && c != 10 }) line.write(c)
-
-    if (c == -1 && line.size == 0) None
-    else {
-      val a = line.toByteArray
-      val n = a.length
-      val len = if (n > 0 && a(n - 1) == 13) n - 1 else n
-      Some(Bytes(a, 0, len))
-    }
+    val line =
+      Bytes.Builder.use(hint = 100) { builder =>
+        while ({ c = stream.read; c != -1 && c != 10 }) {
+          builder += c.toByte
+        }
+      }
+    if (c == -1 && line.size == 0) None else Some(line.trim_line)
   }