clarified store.clean_output: cleanup user_output_dir even in system_mode;
authorwenzelm
Sat May 19 16:13:39 2018 +0200 (14 months ago)
changeset 682208fc4e3d1df86
parent 68219 c0341c0080e2
child 68221 dbef88c2b6c5
clarified store.clean_output: cleanup user_output_dir even in system_mode;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat May 19 15:45:45 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 19 16:13:39 2018 +0200
     1.3 @@ -1004,6 +1004,19 @@
     1.4      def open_output_database(name: String): SQL.Database =
     1.5        SQLite.open_database(output_dir + database(name))
     1.6  
     1.7 +    def clean_output(name: String): (Boolean, Boolean) =
     1.8 +    {
     1.9 +      val res =
    1.10 +        for {
    1.11 +          dir <- (if (system_mode) List(user_output_dir, system_output_dir) else List(user_output_dir))
    1.12 +          file <- List(Path.basic(name), database(name), log(name), log_gz(name))
    1.13 +          path = dir + file if path.is_file
    1.14 +        } yield path.file.delete
    1.15 +      val relevant = res.nonEmpty
    1.16 +      val ok = res.forall(b => b)
    1.17 +      (relevant, ok)
    1.18 +    }
    1.19 +
    1.20  
    1.21      /* input */
    1.22  
     2.1 --- a/src/Pure/Tools/build.scala	Sat May 19 15:45:45 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 16:13:39 2018 +0200
     2.3 @@ -467,19 +467,13 @@
     2.4  
     2.5      store.prepare_output_dir()
     2.6  
     2.7 -    // cleanup
     2.8 -    def cleanup(name: String, echo: Boolean = false)
     2.9 -    {
    2.10 -      val files =
    2.11 -        List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    2.12 -          map(store.output_dir + _).filter(_.is_file)
    2.13 -      if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
    2.14 -      val res = files.map(p => p.file.delete)
    2.15 -      if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
    2.16 -    }
    2.17      if (clean_build) {
    2.18        for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
    2.19 -        cleanup(name, echo = true)
    2.20 +        val (relevant, ok) = store.clean_output(name)
    2.21 +        if (relevant) {
    2.22 +          if (ok) progress.echo("Cleaned " + name)
    2.23 +          else progress.echo(name + " FAILED to clean")
    2.24 +        }
    2.25        }
    2.26      }
    2.27  
    2.28 @@ -618,7 +612,7 @@
    2.29                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
    2.30                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    2.31  
    2.32 -                  cleanup(name)
    2.33 +                  store.clean_output(name)
    2.34                    using(store.open_output_database(name))(store.init_session_info(_, name))
    2.35  
    2.36                    val numa_node = numa_nodes.next(used_node(_))