# HG changeset patch
# User wenzelm
# Date 1718552272 -7200
# Node ID 6f48f96f7997d6bb78d1ba9530ecfe5ce868a177
# Parent  5e8dca75c699f4a51b121ae893f31fc838b8535e
proper treatment of long message blocks;

diff -r 5e8dca75c699 -r 6f48f96f7997 src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Sun Jun 16 14:21:57 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Sun Jun 16 17:37:52 2024 +0200
@@ -27,13 +27,13 @@
 
   /* input operations */
 
-  def read(stream: InputStream, n: Int): Bytes =
+  def read(stream: InputStream, n: Long): Bytes =
     Bytes.read_stream(stream, limit = n)
 
-  def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) = {
+  def read_block(stream: InputStream, n: Long): (Option[Bytes], Long) = {
     val msg = read(stream, n)
     val len = msg.size
-    (if (len == n) Some(msg) else None, len.toInt)
+    (if (len == n) Some(msg) else None, len)
   }
 
   def read_line(stream: InputStream): Option[Bytes] = {
@@ -61,11 +61,13 @@
     flush(stream)
   }
 
-  private def parse_header(line: String): List[Int] =
-    try { space_explode(',', line).map(Value.Nat.parse) }
-    catch { case ERROR(_) => error("Malformed message header: " + quote(line)) }
+  private def parse_header(line: String): List[Long] = {
+    val args = space_explode(',', line)
+    if (args.forall(is_length)) args.map(Value.Long.parse)
+    else error("Malformed message header: " + quote(line))
+  }
 
-  private def read_chunk(stream: InputStream, n: Int): Bytes =
+  private def read_chunk(stream: InputStream, n: Long): Bytes =
     read_block(stream, n) match {
       case (Some(chunk), _) => chunk
       case (None, len) =>
@@ -78,8 +80,13 @@
 
   /* hybrid messages: line or length+block (restricted content) */
 
+  private def is_length(str: String): Boolean =
+    !str.isEmpty && str.iterator.forall(Symbol.is_ascii_digit) &&
+      Value.Long.unapply(str).isDefined
+
   private def is_length(msg: Bytes): Boolean =
-    !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
+    !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) &&
+      Value.Long.unapply(msg.text).isDefined
 
   private def is_terminated(msg: Bytes): Boolean =
     msg.size match {
@@ -103,11 +110,9 @@
 
   def read_line_message(stream: InputStream): Option[Bytes] =
     read_line(stream) match {
-      case None => None
-      case Some(line) =>
-        Value.Nat.unapply(line.text) match {
-          case None => Some(line)
-          case Some(n) => read_block(stream, n)._1.map(_.trim_line)
-        }
+      case Some(line) if is_length(line) =>
+        val n = Value.Long.parse(line.text)
+        read_block(stream, n)._1.map(_.trim_line)
+      case res => res
     }
 }