diff -r 387894c2fb2c -r 704915cf59fa src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Wed Dec 12 00:01:11 2018 +0100
+++ b/src/Pure/PIDE/byte_message.scala	Wed Dec 12 12:31:05 2018 +0100
@@ -24,13 +24,14 @@
 
   /* input operations */
 
-  def read(stream: InputStream, length: Int): Bytes =
-    Bytes.read_stream(stream, limit = length)
+  def read(stream: InputStream, n: Int): Bytes =
+    Bytes.read_stream(stream, limit = n)
 
-  def read_block(stream: InputStream, length: Int): Option[Bytes] =
+  def read_block(stream: InputStream, n: Int): (Option[Bytes], Int) =
   {
-    val msg = read(stream, length)
-    if (msg.length == length) Some(msg) else None
+    val msg = read(stream, n)
+    val len = msg.length
+    (if (len == n) Some(msg) else None, len)
   }
 
   def read_line(stream: InputStream): Option[Bytes] =
@@ -51,11 +52,17 @@
 
   /* header with chunk lengths */
 
+  def write_header(stream: OutputStream, ns: List[Int])
+  {
+    stream.write(UTF8.bytes(ns.mkString(",")))
+    newline(stream)
+  }
+
   private def err_header(line: String): Nothing =
     error("Malformed message header: " + quote(line))
 
   private def parse_header(line: String): List[Int] =
-    try { space_explode(',', line).map(Value.Int.parse_nat) }
+    try { space_explode(',', line).map(Value.Nat.parse) }
     catch { case ERROR(_) => err_header(line) }
 
   def read_header(stream: InputStream): Option[List[Int]] =
@@ -68,12 +75,6 @@
         case _ => err_header(line)
       })
 
-  def write_header(stream: OutputStream, ns: List[Int])
-  {
-    stream.write(UTF8.bytes(ns.mkString(",")))
-    newline(stream)
-  }
-
 
   /* messages with multiple chunks (arbitrary content) */
 
@@ -85,12 +86,11 @@
   }
 
   private def read_chunk(stream: InputStream, n: Int): Bytes =
-  {
-    val chunk = read(stream, n)
-    val len = chunk.length
-    if (len == n) chunk
-    else error("Malformed message chunk: unexpected EOF after " + len + " of " + n + " bytes")
-  }
+    read_block(stream, n) match {
+      case (Some(chunk), _) => chunk
+      case (None, len) =>
+        error("Malformed message chunk: unexpected EOF after " + len + " of " + n + " bytes")
+    }
 
   def read_message(stream: InputStream): Option[List[Bytes]] =
     read_header(stream).map(ns => ns.map(n => read_chunk(stream, n)))
@@ -101,7 +101,7 @@
   private def is_length(msg: Bytes): Boolean =
     !msg.is_empty && msg.iterator.forall(b => Symbol.is_ascii_digit(b.toChar))
 
-  private def has_line_terminator(msg: Bytes): Boolean =
+  private def is_terminated(msg: Bytes): Boolean =
   {
     val len = msg.length
     len > 0 && Symbol.is_ascii_line_terminator(msg.charAt(len - 1))
@@ -109,12 +109,12 @@
 
   def write_line_message(stream: OutputStream, msg: Bytes)
   {
-    if (is_length(msg) || has_line_terminator(msg))
+    if (is_length(msg) || is_terminated(msg))
       error ("Bad content for line message:\n" ++ msg.text.take(100))
 
-    if (msg.length > 100 || msg.iterator.contains(10)) {
-      write_header(stream, List(msg.length + 1))
-    }
+    val n = msg.length
+    if (n > 100 || msg.iterator.contains(10)) write_header(stream, List(n + 1))
+
     write(stream, msg)
     newline(stream)
     flush(stream)
@@ -122,9 +122,11 @@
 
   def read_line_message(stream: InputStream): Option[Bytes] =
     read_line(stream) match {
+      case None => None
       case Some(line) =>
-        if (is_length(line)) read_block(stream, Value.Int.parse(line.text)).map(_.trim_line)
-        else Some(line)
-      case None => None
+        Value.Nat.unapply(line.text) match {
+          case None => Some(line)
+          case Some(n) => read_block(stream, n)._1.map(_.trim_line)
+        }
     }
 }