# HG changeset patch
# User wenzelm
# Date 1673013493 -3600
# Node ID 9ce0aa145d2114656608d9d5ccd10ece411766f3
# Parent  c7a165287df515cb1a731cab2e27fa83dd16deb9
more uniform operations;
plain file_name instead of blob.src_path.implode_short;

diff -r c7a165287df5 -r 9ce0aa145d21 src/Pure/Thy/browser_info.scala
--- a/src/Pure/Thy/browser_info.scala	Fri Jan 06 14:37:55 2023 +0100
+++ b/src/Pure/Thy/browser_info.scala	Fri Jan 06 14:58:13 2023 +0100
@@ -616,13 +616,14 @@
 
       val files =
         for {
-          (blob, xml) <- snapshot.xml_markup_blobs(elements = thy_elements.html)
+          blob_name <- snapshot.node_files.tail
+          xml = snapshot.switch(blob_name).xml_markup(elements = thy_elements.html)
           if xml.nonEmpty
         }
         yield {
           progress.expose_interrupt()
 
-          val file_name = blob.name.node
+          val file_name = blob_name.node
           if (verbose) progress.echo("Presenting file " + quote(file_name))
 
           val file_html = session_dir + context.file_html(file_name)
@@ -630,7 +631,7 @@
           val html_link = HTML.relative_href(file_html, base = Some(session_dir))
           val html = context.source(node_context(file_name, file_dir).make_html(thy_elements, xml))
 
-          val file_title = "File " + Symbol.cartouche_decoded(blob.src_path.implode_short)
+          val file_title = "File " + Symbol.cartouche_decoded(file_name)
           HTML.write_document(file_dir, file_html.file_name,
             List(HTML.title(file_title)), List(context.head(file_title), html),
             root = Some(context.root_dir))
diff -r c7a165287df5 -r 9ce0aa145d21 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jan 06 14:37:55 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Fri Jan 06 14:58:13 2023 +0100
@@ -427,7 +427,8 @@
               cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))),
               compress = false)
 
-            for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
+            for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) {
+              val xml = snapshot.switch(blob_name).xml_markup()
               export_(Export.MARKUP + (i + 1), xml)
             }
             export_(Export.MARKUP, snapshot.xml_markup())