# HG changeset patch
# User wenzelm
# Date 1718108299 -7200
# Node ID 96843eb96493238f7bb490b02d93aa1ec60d7616
# Parent  b5b2f651a2634b9a9db128fd7466d4ec00de417a
clarified signature;

diff -r b5b2f651a263 -r 96843eb96493 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jun 11 14:18:19 2024 +0200
@@ -72,7 +72,7 @@
                   progress.echo(
                     "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
                     verbose = true)
-                  val yxml = YXML.parse_body(UTF8.decode_permissive(msg.chunk), cache = build_results0.cache)
+                  val yxml = YXML.parse_body(msg.chunk.text, cache = build_results0.cache)
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
                     Export.explode_name(args.name) match {
diff -r b5b2f651a263 -r 96843eb96493 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/Pure/Build/build.scala	Tue Jun 11 14:18:19 2024 +0200
@@ -715,7 +715,7 @@
     unicode_symbols: Boolean = false
   ): Option[Document.Snapshot] = {
     def decode_bytes(bytes: Bytes): String =
-      Symbol.output(unicode_symbols, UTF8.decode_permissive(bytes))
+      Symbol.output(unicode_symbols, bytes.text)
 
     def read(name: String): Export.Entry = theory_context(name, permissive = true)
 
diff -r b5b2f651a263 -r 96843eb96493 src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/Pure/Build/export.scala	Tue Jun 11 14:18:19 2024 +0200
@@ -194,7 +194,7 @@
 
     def text: String = bytes.text
 
-    def yxml: XML.Body = YXML.parse_body(UTF8.decode_permissive(bytes), cache = cache)
+    def yxml: XML.Body = YXML.parse_body(bytes.text, cache = cache)
   }
 
   def make_regex(pattern: String): Regex = {
diff -r b5b2f651a263 -r 96843eb96493 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jun 11 14:18:19 2024 +0200
@@ -158,7 +158,7 @@
     a
   }
 
-  def text: String = UTF8.decode_permissive(this)
+  def text: String = UTF8.decode_permissive_bytes(this)
 
   def wellformed_text: Option[String] = {
     val s = text
diff -r b5b2f651a263 -r 96843eb96493 src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Tue Jun 11 11:07:48 2024 +0200
+++ b/src/Pure/General/utf8.scala	Tue Jun 11 14:18:19 2024 +0200
@@ -23,8 +23,8 @@
   // see also https://en.wikipedia.org/wiki/UTF-8#Description
   // overlong encodings enable byte-stuffing of low-ASCII
 
-  def decode_permissive(text: CharSequence): String = {
-    val len = text.length
+  def decode_permissive_bytes(bytes: CharSequence): String = {
+    val len = bytes.length
     val buf = new java.lang.StringBuilder(len)
     var code = -1
     var rest = 0
@@ -51,7 +51,7 @@
       }
     }
     for (i <- 0 until len) {
-      val c = text.charAt(i)
+      val c = bytes.charAt(i)
       if (c < 128) { flush(); buf.append(c) }
       else if ((c & 0xC0) == 0x80) push(c & 0x3F)
       else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
@@ -61,4 +61,7 @@
     flush()
     buf.toString
   }
+
+  def decode_permissive(text: String): String =
+    decode_permissive_bytes(text)
 }