# HG changeset patch
# User wenzelm
# Date 1754423094 -7200
# Node ID e2e43992f339713e443a752be584218c4f9e8d32
# Parent  79d14c86256077acc3c294d423d04f88ecb33fd1
more detailed export "PIDE/files": store offset of the load command, within the pro-forma loaded_theory_command --- this allows to restrict output messages for blobs;
enforce rebuild of Isabelle/ML;

diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/Build/build.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -728,16 +728,17 @@
       val thy_file = migrate_file(thy_file0)
 
       val blobs =
-        blobs_files0.map { name0 =>
+        blobs_files0.map { case (command_offset, name0) =>
           val name = migrate_file(name0)
 
           val file = read_source_file(name0)
           val bytes = file.bytes
           val text = decode(bytes.text)
           val chunk = Symbol.Text_Chunk(text)
+          val content = Some((file.digest, chunk))
 
-          Command.Blob(Document.Node.Name(name), Path.explode(name), Some((file.digest, chunk))) ->
-            Document.Blobs.Item(bytes, text, chunk, changed = false)
+          Command.Blob(command_offset, Document.Node.Name(name), Path.explode(name), content) ->
+            Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
         }
 
       val thy_source = decode(read_source_file(thy_file0).bytes.text)
diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/build_job.scala
--- a/src/Pure/Build/build_job.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -150,20 +150,23 @@
           def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] =
             session_background.base.theory_load_commands.get(node_name.theory) match {
               case None => Nil
-              case Some(spans) =>
+              case Some(load_commands) =>
                 val syntax = session_background.base.theory_syntax(node_name)
                 val master_dir = Path.explode(node_name.master_dir)
-                for (span <- spans; file <- span.loaded_files(syntax).files)
-                  yield {
+                for {
+                  (command_span, command_offset) <- load_commands
+                  file <- command_span.loaded_files(syntax).files
+                } yield {
                     val src_path = Path.explode(file)
                     val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path))
 
                     val bytes = session_sources(blob_name.node).bytes
                     val text = bytes.text
                     val chunk = Symbol.Text_Chunk(text)
+                    val content = Some((SHA1.digest(bytes), chunk))
 
-                    Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) ->
-                      Document.Blobs.Item(bytes, text, chunk, changed = false)
+                    Command.Blob(command_offset, blob_name, src_path, content) ->
+                      Document.Blobs.Item(bytes, text, chunk, command_offset = command_offset)
                   }
             }
 
@@ -307,9 +310,11 @@
                   export_text(Export.DOCUMENT_ID, command.id.toString, compress = false)
                 }
 
-                export_text(Export.FILES,
-                  cat_lines(snapshot.node_files.map(name => File.symbolic_path(name.path))),
-                  compress = false)
+                export_(Export.FILES,
+                  {
+                    import XML.Encode._
+                    list(pair(int, string))(snapshot.node_export_files)
+                  })
 
                 for ((blob_name, i) <- snapshot.node_files.tail.zipWithIndex) {
                   val xml = snapshot.switch(blob_name).xml_markup()
diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/export.scala
--- a/src/Pure/Build/export.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/Build/export.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -502,7 +502,7 @@
       def db_source: Option[String] = {
         val theory_context = session_context.theory(theory)
         for {
-          name <- theory_context.files0(permissive = true).headOption
+          (_, name) <- theory_context.files0(permissive = true).headOption
           file <- get_source_file(name)
         } yield Symbol.output(unicode_symbols, file.bytes.text)
       }
@@ -549,13 +549,15 @@
         case _ => None
       }
 
-    def files0(permissive: Boolean = false): List[String] =
-      split_lines(apply(FILES, permissive = permissive).text)
+    def files0(permissive: Boolean = false): List[(Int, String)] = {
+      import XML.Decode._
+      list(pair(int, string))(apply(FILES, permissive = permissive).yxml())
+    }
 
-    def files(permissive: Boolean = false): Option[(String, List[String])] =
+    def files(permissive: Boolean = false): Option[(String, List[(Int, String)])] =
       files0(permissive = permissive) match {
         case Nil => None
-        case a :: bs => Some((a, bs))
+        case (_, a) :: bs => Some((a, bs))
       }
 
     override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/resources.scala
--- a/src/Pure/Build/resources.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/Build/resources.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -7,6 +7,7 @@
 package isabelle
 
 
+import scala.collection.mutable
 import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
@@ -88,14 +89,20 @@
   def load_commands(
     syntax: Outer_Syntax,
     name: Document.Node.Name
-  ) : () => List[Command_Span.Span] = {
+  ) : () => List[(Command_Span.Span, Symbol.Offset)] = {
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
     () =>
       {
         if (syntax.has_load_commands(raw_text)) {
-          val text = Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text))
-          syntax.parse_spans(text).filter(_.is_load_command(syntax))
+          val spans = syntax.parse_spans(Symbol.decode(Scan.reader_decode_utf8(is_utf8, raw_text)))
+          val result = new mutable.ListBuffer[(Command_Span.Span, Symbol.Offset)]
+          var offset = 1
+          for (span <- spans) {
+            if (span.is_load_command(syntax)) { result += (span -> offset) }
+            offset += span.length
+          }
+          result.toList
         }
         else Nil
       }
@@ -115,7 +122,7 @@
       (file, theory) <- Thy_Header.ml_roots.iterator
       node = append_path("~~/src/Pure", Path.explode(file))
       node_name = Document.Node.Name(node, theory = theory)
-      name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)()).iterator
+      name <- loaded_files(syntax, node_name, load_commands(syntax, node_name)().map(_._1)).iterator
     } yield name).toList
 
   def global_theory(theory: String): Boolean =
@@ -375,9 +382,9 @@
     def get_syntax(name: Document.Node.Name): Outer_Syntax =
       loaded_theories.get_node(name.theory)
 
-    lazy val load_commands: List[(Document.Node.Name, List[Command_Span.Span])] =
+    lazy val load_commands: List[(Document.Node.Name, List[(Command_Span.Span, Symbol.Offset)])] =
       theories.zip(
-        Par_List.map((e: () => List[Command_Span.Span]) => e(),
+        Par_List.map((e: () => List[(Command_Span.Span, Symbol.Offset)]) => e(),
           theories.map(name => resources.load_commands(get_syntax(name), name))))
       .filter(p => p._2.nonEmpty)
 
@@ -394,8 +401,8 @@
 
     def loaded_files: List[Document.Node.Name] =
       for {
-        (name, spans) <- load_commands
-        file <- loaded_files(name, spans)._2
+        (name, cmds) <- load_commands
+        file <- loaded_files(name, cmds.map(_._1))._2
       } yield file
 
     def imported_files: List[Path] = {
diff -r 79d14c862560 -r e2e43992f339 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/Build/sessions.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -102,7 +102,7 @@
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
     used_theories: List[(Document.Node.Name, Options)] = Nil,  // new imports
-    theory_load_commands: Map[String, List[Command_Span.Span]] = Map.empty,
+    theory_load_commands: Map[String, List[(Command_Span.Span, Symbol.Offset)]] = Map.empty,
     known_theories: Map[String, Document.Node.Entry] = Map.empty,
     known_loaded_files: Map[String, List[Path]] = Map.empty,
     overall_syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -301,11 +301,11 @@
                 catch { case ERROR(msg) => (Nil, List(msg)) }
 
               val theory_load_commands =
-                (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap
+                (for ((name, cmd) <- load_commands.iterator) yield name.theory -> cmd).toMap
 
               val loaded_files: List[(String, List[Path])] =
-                for ((name, spans) <- load_commands) yield {
-                  val (theory, files) = dependencies.loaded_files(name, spans)
+                for ((name, cmds) <- load_commands) yield {
+                  val (theory, files) = dependencies.loaded_files(name, cmds.map(_._1))
                   theory -> files.map(file => Path.explode(file.node))
                 }
 
diff -r 79d14c862560 -r e2e43992f339 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -15,6 +15,7 @@
   /* blobs */
 
   sealed case class Blob(
+    command_offset: Symbol.Offset,
     name: Document.Node.Name,
     src_path: Path,
     content: Option[(SHA1.Digest, Symbol.Text_Chunk)]
@@ -454,7 +455,7 @@
               val src_path = Path.explode(file)
               val name = Document.Node.Name(resources.append_path(node_name.master_dir, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
-              Blob(name, src_path, content)
+              Blob(0, name, src_path, content)
             }).user_error)
         Blobs_Info(blobs, index = loaded_files.index)
     }
@@ -496,6 +497,9 @@
   def blobs_names: List[Document.Node.Name] =
     for (case Exn.Res(blob) <- blobs) yield blob.name
 
+  def blobs_files: List[(Symbol.Offset, Document.Node.Name)] =
+    for (case Exn.Res(blob) <- blobs) yield (blob.command_offset, blob.name)
+
   def blobs_undefined: List[Document.Node.Name] =
     for (case Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
 
diff -r 79d14c862560 -r e2e43992f339 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -46,7 +46,8 @@
       bytes: Bytes,
       source: String,
       chunk: Symbol.Text_Chunk,
-      changed: Boolean
+      command_offset: Symbol.Offset = 0,
+      changed: Boolean = false
     ) {
       def source_wellformed: Boolean = bytes.wellformed_text.nonEmpty
       def unchanged: Item = if (changed) copy(changed = false) else this
@@ -588,6 +589,10 @@
     def node_files: List[Node.Name] =
       node_name :: node.load_commands.flatMap(_.blobs_names)
 
+    def node_export_files: List[(Symbol.Offset, String)] =
+      for ((i, name) <- (0, node_name) :: node.load_commands.flatMap(_.blobs_files))
+        yield (i, File.symbolic_path(name.path))
+
     def node_consolidated(name: Node.Name): Boolean =
       state.node_consolidated(version, name)
 
@@ -605,7 +610,16 @@
           case _ => None
         }
       }
-      else None
+      else {
+        for {
+          command <- version.nodes.commands_loading(node_name).find(_.span.is_theory)
+          (symbol_offset, _) <- command.blobs_files.find({ case (_, name) => node_name == name })
+        } yield {
+          val chunk_offset = command.chunk.decode(symbol_offset)
+          val command_range = switch(command.node_name).command_range(Text.Range(chunk_offset))
+          command -> command_range.getOrElse(Text.Range.offside)
+        }
+      }
 
 
     /* pending edits */
diff -r 79d14c862560 -r e2e43992f339 src/Pure/PIDE/document_info.scala
--- a/src/Pure/PIDE/document_info.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/PIDE/document_info.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -103,7 +103,7 @@
             Theory(theory_name,
               static_session = sessions_structure.theory_qualifier(theory_name),
               dynamic_session = session_name,
-              files = files,
+              files = files.map(_._2),
               entities = theory_export.entity_iterator.toList,
               others = theory_export.others.keySet.toList)
           Some(theory)
diff -r 79d14c862560 -r e2e43992f339 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 05 21:44:54 2025 +0200
@@ -346,7 +346,7 @@
     val blobs_xml: XML.Body = {
       val encode_blob: T[Exn.Result[Command.Blob]] =
         variant(List(
-          { case Exn.Res(Command.Blob(a, b, c)) =>
+          { case Exn.Res(Command.Blob(_, a, b, c)) =>
               (Nil, triple(string, string, option(string))(
                 (a.node, b.implode, c.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
diff -r 79d14c862560 -r e2e43992f339 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 05 16:04:05 2025 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 05 21:44:54 2025 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ROOT.ML
     Author:     Makarius
-    UUID:       a83d12be-3568-49ab-9484-a84de5cee2bf
+    UUID:       65c4f1c9-5db7-4528-b719-40dbb49a0791
 
 Main entry point for the Isabelle/Pure bootstrap process.