# HG changeset patch
# User wenzelm
# Date 1526739219 -7200
# Node ID 8fc4e3d1df86a269a0bd2966913cd3ab0a278acf
# Parent  c0341c0080e24e18591766d6eef7dd3096502702
clarified store.clean_output: cleanup user_output_dir even in system_mode;

diff -r c0341c0080e2 -r 8fc4e3d1df86 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat May 19 15:45:45 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat May 19 16:13:39 2018 +0200
@@ -1004,6 +1004,19 @@
     def open_output_database(name: String): SQL.Database =
       SQLite.open_database(output_dir + database(name))
 
+    def clean_output(name: String): (Boolean, Boolean) =
+    {
+      val res =
+        for {
+          dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
+          file <- List(Path.basic(name), database(name), log(name), log_gz(name))
+          path = dir + file if path.is_file
+        } yield path.file.delete
+      val relevant = res.nonEmpty
+      val ok = res.forall(b => b)
+      (relevant, ok)
+    }
+
 
     /* input */
 
diff -r c0341c0080e2 -r 8fc4e3d1df86 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat May 19 15:45:45 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 19 16:13:39 2018 +0200
@@ -467,19 +467,13 @@
 
     store.prepare_output_dir()
 
-    // cleanup
-    def cleanup(name: String, echo: Boolean = false)
-    {
-      val files =
-        List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
-          map(store.output_dir + _).filter(_.is_file)
-      if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
-      val res = files.map(p => p.file.delete)
-      if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
-    }
     if (clean_build) {
       for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
-        cleanup(name, echo = true)
+        val (relevant, ok) = store.clean_output(name)
+        if (relevant) {
+          if (ok) progress.echo("Cleaned " + name)
+          else progress.echo(name + " FAILED to clean")
+        }
       }
     }
 
@@ -618,7 +612,7 @@
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
 
-                  cleanup(name)
+                  store.clean_output(name)
                   using(store.open_output_database(name))(store.init_session_info(_, name))
 
                   val numa_node = numa_nodes.next(used_node(_))