Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Fri, 19 Aug 2022 20:19:05 +0200
changeset 75909 198a52d26b57
parent 75908 6b979348455e
child 75910 529e4ac56904
tuned signature;
src/Pure/PIDE/document.scala file | annotate | diff | comparison | revisions
src/Pure/Tools/build_job.scala file | annotate | diff | comparison | revisions 
--- 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
 
--- 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)
isabelle