# HG changeset patch
# User wenzelm
# Date 1489695721 -3600
# Node ID b553d0edc440e53291b8ad12b16d14342306df61
# Parent  e9f9f962828da4f768060529c5b1533376a7f5a3
tuned signature;

diff -r e9f9f962828d -r b553d0edc440 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 16 21:09:13 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 21:22:01 2017 +0100
@@ -515,13 +515,16 @@
 
   /** persistent store **/
 
-  def log(name: String): Path = Path.basic("log") + Path.basic(name)
-  def log_gz(name: String): Path = log(name).ext("gz")
-
   def store(system_mode: Boolean = false): Store = new Store(system_mode)
 
   class Store private[Sessions](system_mode: Boolean)
   {
+    /* file names */
+
+    def log(name: String): Path = Path.basic("log") + Path.basic(name)
+    def log_gz(name: String): Path = log(name).ext("gz")
+
+
     /* output */
 
     val browser_info: Path =
diff -r e9f9f962828d -r b553d0edc440 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 16 21:09:13 2017 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 16 21:22:01 2017 +0100
@@ -372,7 +372,7 @@
     if (clean_build) {
       for (name <- full_tree.graph.all_succs(selected)) {
         val files =
-          List(Path.basic(name), Sessions.log(name), Sessions.log_gz(name)).
+          List(Path.basic(name), store.log(name), store.log_gz(name)).
             map(store.output_dir + _).filter(_.is_file)
         if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
         if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
@@ -429,18 +429,18 @@
               val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
               process_result.copy(
                 out_lines =
-                  "(see also " + (store.output_dir + Sessions.log(name)).file.toString + ")" ::
+                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
                   lines1)
             }
 
             val heap_stamp =
               if (process_result.ok) {
-                (store.output_dir + Sessions.log(name)).file.delete
+                (store.output_dir + store.log(name)).file.delete
                 val heap_stamp =
                   for (path <- job.output_path if path.is_file)
                     yield Sessions.write_heap_digest(path)
 
-                File.write_gzip(store.output_dir + Sessions.log_gz(name),
+                File.write_gzip(store.output_dir + store.log_gz(name),
                   terminate_lines(
                     session_sources_stamp(name) ::
                     input_heaps.map(INPUT_HEAP + _) :::
@@ -451,9 +451,9 @@
               }
               else {
                 (store.output_dir + Path.basic(name)).file.delete
-                (store.output_dir + Sessions.log_gz(name)).file.delete
+                (store.output_dir + store.log_gz(name)).file.delete
 
-                File.write(store.output_dir + Sessions.log(name),
+                File.write(store.output_dir + store.log(name),
                   terminate_lines(process_result.out_lines))
                 progress.echo(name + " FAILED")
                 if (!process_result.interrupted) progress.echo(process_result_tail.out)