src/Pure/General/bytes.scala

 
 package isabelle
 
 
 import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream,
-  InputStream, OutputStream, File => JFile}
+  InputStreamReader, InputStream, OutputStream, File => JFile}
 import java.nio.ByteBuffer
 import java.nio.charset.StandardCharsets.ISO_8859_1
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
 import java.util.Arrays

 
 object Bytes {
   /* internal sizes */
 
   private val array_size: Long = Int.MaxValue - 8  // see java.io.InputStream.MAX_BUFFER_SIZE
+  private val string_size: Long = Int.MaxValue / 2
   private val block_size: Int = 16384  // see java.io.InputStream.DEFAULT_BUFFER_SIZE
   private val chunk_size: Long = Space.MiB(100).bytes
 
   private def make_size(chunks: Array[Array[Byte]], buffer: Array[Byte]): Long =
     chunks.foldLeft(buffer.length.toLong)((n, chunk) => n + chunk.length)

     val buf = new ByteArrayOutputStream(small_size)
     for (a <- subarray_iterator) { buf.write(a.array, a.offset, a.length) }
     buf.toByteArray
   }
 
-  override def text: String =
+  def text: String =
     if (is_empty) ""
     else {
-      var i = 0L
-      var utf8 = false
-      while (i < size && !utf8) {
-        if (byte_unchecked(i) < 0) { utf8 = true }
-        i += 1
-      }
-      utf8
-
-      if (utf8) UTF8.decode_permissive(bytes)
-      else new String(make_array, UTF8.charset)
+      val reader = new InputStreamReader(stream(), UTF8.charset)
+      val buf = new Array[Char]((size min Bytes.string_size).toInt + 1)
+      var m = 0
+      var n = 0
+      while (m >= 0 && n < buf.length) {
+        m = reader.read(buf, n, (buf.length - n) min Bytes.block_size)
+        if (m > 0) { n += m }
+      }
+      require(m == -1, "Malformed UTF-8 string: overlong result")
+      new String(buf, 0, n)
     }
 
   def wellformed_text: Option[String] =
     try {
       val s = text