src/Pure/Tools/build_job.scala
changeset 76872 8b98cffb1a99
parent 76871 a17f9ff37558
child 76873 713eb7f2230e
--- 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)