# HG changeset patch
# User wenzelm
# Date 1660933145 -7200
# Node ID 198a52d26b57980c267486c025ba3348ea741c40
# Parent  6b979348455ebef0a58504ab63c35f2813d7afff
tuned signature;

diff -r 6b979348455e -r 198a52d26b57 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 19 20:11:15 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 19 20:19:05 2022 +0200
@@ -116,8 +116,6 @@
 
       def expand: Name =
         Name(path.expand.implode, master_dir_path.expand.implode, theory)
-      def symbolic: Name =
-        Name(path.implode_symbolic, master_dir_path.implode_symbolic, theory)
 
       def is_theory: Boolean = theory.nonEmpty
 
diff -r 6b979348455e -r 198a52d26b57 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Aug 19 20:11:15 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Aug 19 20:19:05 2022 +0200
@@ -364,7 +364,7 @@
             }
 
             export_text(Export.FILES,
-              cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false)
+              cat_lines(snapshot.node_files.map(_.path.implode_symbolic)), compress = false)
 
             for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) {
               export_(Export.MARKUP + (i + 1), xml)