# 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()