--- a/src/Pure/Thy/sessions.scala Mon Jan 02 16:02:16 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Jan 02 20:24:43 2023 +0100
@@ -122,7 +122,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
- load_commands: Map[Document.Node.Name, List[Command_Span.Span]] = Map.empty,
+ theory_load_commands: Map[String, List[Command_Span.Span]] = 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,
@@ -351,6 +351,9 @@
try { if (inlined_files) (dependencies.load_commands, Nil) else (Nil, Nil) }
catch { case ERROR(msg) => (Nil, List(msg)) }
+ val theory_load_commands =
+ (for ((name, span) <- load_commands.iterator) yield name.theory -> span).toMap
+
val loaded_files =
load_commands.map({ case (name, spans) => dependencies.loaded_files(name, spans) })
@@ -506,7 +509,7 @@
document_theories = document_theories,
loaded_theories = dependencies.loaded_theories,
used_theories = dependencies.theories_adjunct,
- load_commands = load_commands.toMap,
+ theory_load_commands = theory_load_commands,
known_theories = known_theories,
known_loaded_files = known_loaded_files,
overall_syntax = overall_syntax,
--- a/src/Pure/Tools/build_job.scala Mon Jan 02 16:02:16 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Jan 02 20:24:43 2023 +0100
@@ -276,8 +276,7 @@
override val cache: Term.Cache = store.cache
override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
- val expand_node = Document.Node.Name(Path.explode(name.node).expand.implode)
- session_background.base.load_commands.get(expand_node) match {
+ session_background.base.theory_load_commands.get(name.theory) match {
case Some(spans) =>
val syntax = session_background.base.theory_syntax(name)
Command.build_blobs_info(syntax, name, spans)