# HG changeset patch
# User wenzelm
# Date 1525521411 -7200
# Node ID 9e1c670301b82f7fcaccc278538f10493a3a16de
# Parent  b25ccd85b1fd2f696ab487cbb18085172b711d92
cleanup session output before starting build job;
tuned signature;

diff -r b25ccd85b1fd -r 9e1c670301b8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri May 04 22:26:25 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat May 05 13:56:51 2018 +0200
@@ -1003,6 +1003,10 @@
 
     def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
 
+    def output_database(name: String): Path = output_dir + database(name)
+    def output_log(name: String): Path = output_dir + log(name)
+    def output_log_gz(name: String): Path = output_dir + log_gz(name)
+
 
     /* input */
 
@@ -1028,6 +1032,15 @@
 
     /* session info */
 
+    def init_session_info(db: SQL.Database, name: String)
+    {
+      db.transaction {
+        db.create_table(Session_Info.table)
+        db.using_statement(
+          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
+      }
+    }
+
     def write_session_info(
       db: SQL.Database,
       name: String,
@@ -1035,9 +1048,6 @@
       build: Build.Session_Info)
     {
       db.transaction {
-        db.create_table(Session_Info.table)
-        db.using_statement(
-          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
         db.using_statement(Session_Info.table.insert())(stmt =>
         {
           stmt.string(1) = name
diff -r b25ccd85b1fd -r 9e1c670301b8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri May 04 22:26:25 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat May 05 13:56:51 2018 +0200
@@ -32,10 +32,11 @@
 
   private object Queue
   {
-    def load_timings(progress: Progress, store: Sessions.Store, name: String)
-      : (List[Properties.T], Double) =
+    type Timings = (List[Properties.T], Double)
+
+    def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings =
     {
-      val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
+      val no_timings: Timings = (Nil, 0.0)
 
       store.find_database(name) match {
         case None => no_timings
@@ -184,7 +185,6 @@
   {
     val output = store.output_dir + Path.basic(name)
     def output_path: Option[Path] = if (do_output) Some(output) else None
-    output.file.delete
 
     val options =
       numa_node match {
@@ -448,14 +448,19 @@
 
     store.prepare_output()
 
-    // optional cleanup
+    // 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))) {
-        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("Cleaning " + name + " ...")
-        if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
+        cleanup(name, echo = true)
       }
     }
 
@@ -507,7 +512,7 @@
               val tail = job.info.options.int("process_output_tail")
               process_result.copy(
                 out_lines =
-                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
+                  "(see also " + store.output_log(name).file.toString + ")" ::
                   (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
             }
 
@@ -515,29 +520,22 @@
             // write log file
             val heap_stamp =
               if (process_result.ok) {
-                (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 + store.log_gz(name), terminate_lines(log_lines))
+                File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
 
                 heap_stamp
               }
               else {
-                (store.output_dir + Path.basic(name)).file.delete
-                (store.output_dir + store.log_gz(name)).file.delete
-
-                File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
+                File.write(store.output_log(name), terminate_lines(log_lines))
 
                 None
               }
 
             // write database
             {
-              val database = store.output_dir + store.database(name)
-              database.file.delete
-
               val build_log =
                 Build_Log.Log_File(name, process_result.out_lines).
                   parse_session_info(
@@ -546,7 +544,7 @@
                     ml_statistics = true,
                     task_statistics = true)
 
-              using(SQLite.open_database(database))(db =>
+              using(SQLite.open_database(store.output_database(name)))(db =>
                 store.write_session_info(db, name,
                   build_log =
                     if (process_result.timeout) build_log.error("Timeout") else build_log,
@@ -609,8 +607,13 @@
                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
+                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
+
+                  cleanup(name)
+                  using(SQLite.open_database(store.output_database(name)))(db =>
+                    store.init_session_info(db, name))
+
                   val numa_node = numa_nodes.next(used_node(_))
-                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
                     new Job(progress, name, info, selected_sessions, deps, store, do_output,
                       verbose, pide, numa_node, queue.command_timings(name))