# HG changeset patch
# User wenzelm
# Date 1671302654 -3600
# Node ID 32c0abd3507164395d20cda8f07dcc2aecc3ada5
# Parent  254964ca1b9844f593c37c8ff10943ca39889dc2
clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);

diff -r 254964ca1b98 -r 32c0abd35071 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 17 19:35:49 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 17 19:44:14 2022 +0100
@@ -117,9 +117,6 @@
       def path: Path = Path.explode(File.standard_path(node))
       def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
 
-      def expand: Name =
-        Name(path.expand.implode, master_dir_path.expand.implode, theory)
-
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
diff -r 254964ca1b98 -r 32c0abd35071 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Sat Dec 17 19:35:49 2022 +0100
+++ b/src/Pure/Tools/build_job.scala	Sat Dec 17 19:44:14 2022 +0100
@@ -276,7 +276,8 @@
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = {
-            session_background.base.load_commands.get(name.expand) match {
+            val name1 = name.map(s => Path.explode(s).expand.implode)
+            session_background.base.load_commands.get(name1) match {
               case Some(spans) =>
                 val syntax = session_background.base.theory_syntax(name)
                 Command.build_blobs_info(syntax, name, spans)