more robust: prefer internal theory names;
authorwenzelm
Mon, 02 Jan 2023 20:24:43 +0100
changeset 76872 8b98cffb1a99
parent 76871 a17f9ff37558
child 76873 713eb7f2230e
more robust: prefer internal theory names;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build_job.scala
--- 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)