# HG changeset patch
# User wenzelm
# Date 1719954815 -7200
# Node ID 972f7a4cdc0e822f69bf28887159e8cb8c969341
# Parent  762fcf8f9cedaf01ffb63237ec982a8184641ee4
clarified YXML.Source: more direct support for String and Bytes, instead of CharSequence;

diff -r 762fcf8f9ced -r 972f7a4cdc0e src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -72,7 +72,7 @@
                   progress.echo(
                     "Mirabelle export " + quote(args.compound_name) + " (in " + session_name + ")",
                     verbose = true)
-                  val yxml = YXML.parse_body(msg.chunk.text, cache = build_results0.cache)
+                  val yxml = YXML.parse_body(msg.chunk, cache = build_results0.cache)
                   val lines = Pretty.string_of(yxml).trim()
                   val prefix =
                     Export.explode_name(args.name) match {
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -154,7 +154,8 @@
     def apply(args: String): String = {
       val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) = {
         import XML.Decode._
-        pair(int, pair(bool, pair(int, pair(int, string))))(YXML.parse_body(args))
+        pair(int, pair(bool, pair(int, pair(int, string))))(
+          YXML.parse_body(YXML.Source(args)))
       }
       val result =
         execute(kki,
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -237,7 +237,9 @@
     /* properties (YXML) */
 
     def parse_props(text: String): Properties.T =
-      try { cache.props(XML.Decode.properties(YXML.parse_body(text, cache = cache))) }
+      try {
+        cache.props(XML.Decode.properties(YXML.parse_body(YXML.Source(text), cache = cache)))
+      }
       catch { case _: XML.Error => log_file.err("malformed properties") }
 
     def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
@@ -658,7 +660,7 @@
     if (bytes.is_empty) Nil
     else {
       XML.Decode.list(YXML.string_of_body(_))(
-        YXML.parse_body(bytes.uncompress(cache = cache.compress).text, cache = cache))
+        YXML.parse_body(bytes.uncompress(cache = cache.compress), cache = cache))
     }
 
 
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Build/build.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -719,7 +719,7 @@
     def read(name: String): Export.Entry = theory_context(name, permissive = true)
 
     def read_xml(name: String): XML.Body =
-      YXML.parse_body(read(name).bytes.text, recode = decode, cache = theory_context.cache)
+      YXML.parse_body(read(name).bytes, recode = decode, cache = theory_context.cache)
 
     def read_source_file(name: String): Store.Source_File =
       theory_context.session_context.source_file(name)
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Build/build_schedule.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -549,7 +549,7 @@
           Schedule(build_uuid, generator, start, graph, serial)
         }
 
-      schedule(YXML.parse_body(File.read(file)))
+      schedule(YXML.parse_body(Bytes.read(file)))
     }
   }
 
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Build/export.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -195,7 +195,7 @@
     def text: String = bytes.text
 
     def yxml(recode: String => String = identity): XML.Body =
-      YXML.parse_body(bytes.text, recode = recode, cache = cache)
+      YXML.parse_body(bytes, recode = recode, cache = cache)
   }
 
   def make_regex(pattern: String): Regex = {
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -292,7 +292,7 @@
   protected val chunk0: Array[Byte],
   protected val offset: Long,
   val size: Long
-) extends Bytes.Vec {
+) extends Bytes.Vec with YXML.Source {
   assert(
     (chunks.isEmpty ||
       chunks.get.nonEmpty &&
@@ -303,7 +303,7 @@
     if (size > Bytes.array_size) throw new Bytes.Too_Large(size)
     else size.toInt
 
-  def is_empty: Boolean = size == 0
+  override def is_empty: Boolean = size == 0
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
 
@@ -423,6 +423,12 @@
 
   def split_lines: List[Bytes] = space_explode(10)
 
+  // YXML.Source operations
+  override def is_X: Boolean = size == 1 && byte_unchecked(0) == YXML.X_byte
+  override def is_Y: Boolean = size == 1 && byte_unchecked(0) == YXML.Y_byte
+  override def iterator_X: Iterator[Bytes] = separated_chunks(YXML.X_byte)
+  override def iterator_Y: Iterator[Bytes] = separated_chunks(YXML.Y_byte)
+
 
   /* hash and equality */
 
@@ -478,7 +484,7 @@
     buf.toByteArray
   }
 
-  def text: String =
+  override def text: String =
     if (is_empty) ""
     else {
       var i = 0L
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/output.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -9,7 +9,7 @@
 
 object Output {
   def clean_yxml(msg: String): String =
-    try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) }
+    try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(YXML.Source(msg)))) }
     catch { case ERROR(_) => msg }
 
   def writeln_text(msg: String): String = clean_yxml(msg)
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/properties.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -50,7 +50,7 @@
 
   def decode(bs: Bytes, cache: XML.Cache = XML.Cache.none): T = {
     if (bs.is_empty) Nil
-    else cache.props(XML.Decode.properties(YXML.parse_body(bs.text)))
+    else cache.props(XML.Decode.properties(YXML.parse_body(bs)))
   }
 
   def compress(ps: List[T],
@@ -69,7 +69,7 @@
     else {
       val ps =
         XML.Decode.list(XML.Decode.properties)(
-          YXML.parse_body(bs.uncompress(cache = cache.compress).text))
+          YXML.parse_body(bs.uncompress(cache = cache.compress)))
       if (cache.no_cache) ps else ps.map(cache.props)
     }
   }
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -541,10 +541,10 @@
   def encode(text: String): String = symbols.encode(text)
 
   def decode_yxml(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
-    YXML.parse_body(text, recode = decode, cache = cache)
+    YXML.parse_body(YXML.Source(text), recode = decode, cache = cache)
 
   def decode_yxml_failsafe(text: String, cache: XML.Cache = XML.Cache.none): XML.Body =
-    YXML.parse_body_failsafe(text, recode = decode, cache = cache)
+    YXML.parse_body_failsafe(YXML.Source(text), recode = decode, cache = cache)
 
   def encode_yxml(body: XML.Body): String =
     YXML.string_of_body(body, recode = encode)
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/PIDE/yxml.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -93,16 +93,40 @@
     if (name == "") err("unbalanced element")
     else err("unbalanced element " + quote(name))
 
+  object Source {
+    def apply(s: String): Source = new Source_String(s)
+  }
+
+  trait Source {
+    def is_empty: Boolean
+    def is_X: Boolean
+    def is_Y: Boolean
+    def iterator_X: Iterator[Source]
+    def iterator_Y: Iterator[Source]
+    def text: String
+  }
+
+  class Source_String(source: String) extends Source {
+    override def is_empty: Boolean = source.isEmpty
+    override def is_X: Boolean = source.length == 1 && source(0) == X
+    override def is_Y: Boolean = source.length == 1 && source(0) == Y
+    override def iterator_X: Iterator[Source] =
+      Library.separated_chunks(X, source).map(Source.apply)
+    override def iterator_Y: Iterator[Source] =
+      Library.separated_chunks(Y, source).map(Source.apply)
+    override def text: String = source
+  }
+
   def parse_body(
-    source: CharSequence,
+    source: Source,
     recode: String => String = identity,
     cache: XML.Cache = XML.Cache.none
   ): XML.Body = {
     /* parse + recode */
 
-    def parse_string(s: CharSequence): String = recode(s.toString)
+    def parse_string(s: Source): String = recode(s.text)
 
-    def parse_attrib(s: CharSequence): (String, String) =
+    def parse_attrib(s: Source): (String, String) =
       Properties.Eq.unapply(parse_string(s)) getOrElse err_attribute()
 
 
@@ -129,11 +153,11 @@
 
     /* parse chunks */
 
-    for (chunk <- Library.separated_chunks(is_X, source) if chunk.length != 0) {
-      if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
+    for (chunk <- source.iterator_X if !chunk.is_empty) {
+      if (chunk.is_Y) pop()
       else {
-        Library.separated_chunks(is_Y, chunk).toList match {
-          case ch :: name :: atts if ch.length == 0 =>
+        chunk.iterator_Y.toList match {
+          case ch :: name :: atts if ch.is_empty =>
             push(parse_string(name), atts.map(parse_attrib))
           case txts =>
             for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt)))))
@@ -147,7 +171,7 @@
   }
 
   def parse(
-    source: CharSequence,
+    source: Source,
     recode: String => String = identity,
     cache: XML.Cache = XML.Cache.none
   ): XML.Tree =
@@ -158,7 +182,7 @@
     }
 
   def parse_elem(
-    source: CharSequence,
+    source: Source,
     recode: String => String = identity,
     cache: XML.Cache = XML.Cache.none
   ): XML.Tree =
@@ -170,11 +194,11 @@
 
   /* failsafe parsing */
 
-  private def markup_broken(source: CharSequence) =
+  private def markup_broken(source: Source) =
     XML.Elem(Markup.Broken, List(XML.Text(source.toString)))
 
   def parse_body_failsafe(
-    source: CharSequence,
+    source: Source,
     recode: String => String = identity,
     cache: XML.Cache = XML.Cache.none
   ): XML.Body = {
@@ -183,7 +207,7 @@
   }
 
   def parse_failsafe(
-    source: CharSequence,
+    source: Source,
     recode: String => String = identity,
     cache: XML.Cache = XML.Cache.none
   ): XML.Tree = {
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/System/bash.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -370,14 +370,14 @@
             Bash.process(script,
               description = description,
               cwd =
-                XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match {
+                XML.Decode.option(XML.Decode.string)(YXML.parse_body(YXML.Source(cwd))) match {
                   case None => Path.current
                   case Some(s) => Path.explode(s)
                 },
               env =
                 Isabelle_System.settings(
                   XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))(
-                    YXML.parse_body(putenv))),
+                    YXML.parse_body(YXML.Source(putenv)))),
               redirect = redirect)
           }
           match {
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -248,7 +248,7 @@
         val body =
           if (selected) {
             val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
-            YXML.parse_body(entry.text)
+            YXML.parse_body(entry.bytes)
           }
           else {
             val text =
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Tools/profiling.scala
--- a/src/Pure/Tools/profiling.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Tools/profiling.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -89,7 +89,7 @@
             ML_Process.session_heaps(store, session_background, logic = session_name)
           ML_Process(store.options, session_background, session_heaps, args = eval_args,
             env = Isabelle_System.settings(put_env)).result().check
-          decode_result(YXML.parse_body(File.read(dir + Path.explode("result.yxml"))))
+          decode_result(YXML.parse_body(Bytes.read(dir + Path.explode("result.yxml"))))
         }
       }
 
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Tools/server.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -46,7 +46,7 @@
 
     def parse(argument: String): Any =
       if (argument == "") ()
-      else if (YXML.detect_elem(argument)) YXML.parse_elem(argument)
+      else if (YXML.detect_elem(argument)) YXML.parse_elem(YXML.Source(argument))
       else JSON.parse(argument, strict = false)
 
     def unapply(argument: String): Option[Any] =
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Pure/Tools/update_tool.scala
--- a/src/Pure/Tools/update_tool.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Pure/Tools/update_tool.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -115,7 +115,8 @@
               if snapshot.node.source_wellformed
             } {
               progress.expose_interrupt()
-              val xml = YXML.parse_body(YXML.string_of_body(snapshot.xml_markup(elements = update_elements)))
+              val xml =
+                YXML.parse_body(YXML.bytes_of_body(snapshot.xml_markup(elements = update_elements)))
               val source1 = XML.content(update_xml(session_options, xml))
               if (source1 != snapshot.node.source) {
                 val path = Path.explode(node_name.node)
diff -r 762fcf8f9ced -r 972f7a4cdc0e src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jul 02 22:38:00 2024 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jul 02 23:13:35 2024 +0200
@@ -223,9 +223,9 @@
             case Exn.Res(_) =>
               List(Protocol.writeln_message("DONE"))
             case Exn.Exn(exn: Document_Build.Build_Error) =>
-              exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
+              exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(YXML.Source(s))))
             case Exn.Exn(exn) =>
-              List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
+              List(Protocol.error_message(YXML.parse_body(YXML.Source(Exn.print(exn)))))
           }
 
         progress.stop_program()