# HG changeset patch
# User wenzelm
# Date 1493394228 -7200
# Node ID 325801edb37dcbfa07df6980b26e1e1092a62877
# Parent  cfcafe9824d1b1c336b49be198580d7e15b4de80
clarified transaction boundaries: more robust incremental write operations;

diff -r cfcafe9824d1 -r 325801edb37d src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Apr 28 17:17:23 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Apr 28 17:43:48 2017 +0200
@@ -640,31 +640,35 @@
 
     def filter_files(db: SQL.Database, table: SQL.Table, files: List[JFile]): List[JFile] =
     {
-      val key = Meta_Info.log_name
-      val known_files =
-        using(db.select_statement(table, List(key)))(stmt =>
-          SQL.iterator(stmt.executeQuery)(rs => db.string(rs, key)).toSet)
+      db.transaction {
+        db.create_table(table)
+
+        val key = Meta_Info.log_name
+        val known_files =
+          using(db.select_statement(table, List(key)))(stmt =>
+            SQL.iterator(stmt.executeQuery)(rs => db.string(rs, key)).toSet)
 
-      val unique_files =
-        (Map.empty[String, JFile] /: files.iterator)({ case (m, file) =>
-          val name = Log_File.plain_name(file.getName)
-          if (known_files(name)) m else m + (name -> file)
-        })
+        val unique_files =
+          (Map.empty[String, JFile] /: files.iterator)({ case (m, file) =>
+            val name = Log_File.plain_name(file.getName)
+            if (known_files(name)) m else m + (name -> file)
+          })
 
-      unique_files.iterator.map(_._2).toList
+        unique_files.iterator.map(_._2).toList
+      }
     }
 
     def write_meta_info(db: SQL.Database, files: List[JFile])
     {
-      db.transaction {
-        db.create_table(Meta_Info.table)
+      for (file <- filter_files(db, Meta_Info.table, files)) {
+        val log_file = Log_File(file)
+        val meta_info = log_file.parse_meta_info()
 
-        using(db.insert_statement(Meta_Info.table))(stmt =>
-        {
-          for (file <- filter_files(db, Meta_Info.table, files)) {
-            val log_file = Log_File(file)
-            val meta_info = log_file.parse_meta_info()
-
+        db.transaction {
+          using(db.delete_statement(
+            Meta_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
+          using(db.insert_statement(Meta_Info.table))(stmt =>
+          {
             db.set_string(stmt, 1, log_file.name)
             for ((c, i) <- Meta_Info.table.columns.tail.zipWithIndex) {
               if (c.T == SQL.Type.Date)
@@ -672,23 +676,23 @@
               else
                 db.set_string(stmt, i + 2, meta_info.get(c).map(Prop.multiple_lines(_)).orNull)
             }
-
             stmt.execute()
-          }
-        })
+          })
+        }
       }
     }
 
     def write_build_info(db: SQL.Database, files: List[JFile])
     {
-      db.transaction {
-        db.create_table(Build_Info.table)
+      for (file <- filter_files(db, Build_Info.table, files)) {
+        val log_file = Log_File(file)
+        val build_info = log_file.parse_build_info()
 
-        using(db.insert_statement(Build_Info.table))(stmt =>
-        {
-          for (file <- filter_files(db, Build_Info.table, files)) {
-            val log_file = Log_File(file)
-            val build_info = log_file.parse_build_info()
+        db.transaction {
+          using(db.delete_statement(
+            Build_Info.table, Meta_Info.log_name.sql_where_equal(log_file.name)))(_.execute)
+          using(db.insert_statement(Build_Info.table))(stmt =>
+          {
             for ((session_name, session) <- build_info.sessions.iterator) {
               db.set_string(stmt, 1, log_file.name)
               db.set_string(stmt, 2, session_name)
@@ -702,8 +706,8 @@
               db.set_string(stmt, 10, session.status.toString)
               stmt.execute()
             }
-          }
-        })
+          })
+        }
       }
     }
   }