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] = {