more direct insert_permissive statement, which avoids somewhat fragile nested transactions;

--- a/src/Pure/Admin/build_log.scala	Wed May 03 17:00:50 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 03 23:04:25 2017 +0200
@@ -796,20 +796,17 @@
       val meta_info = log_file.parse_meta_info()
       val table = Data.meta_info_table
 
-      db.transaction {
-        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
-        db.using_statement(table.insert())(stmt =>
-        {
-          db.set_string(stmt, 1, log_file.name)
-          for ((c, i) <- table.columns.tail.zipWithIndex) {
-            if (c.T == SQL.Type.Date)
-              db.set_date(stmt, i + 2, meta_info.get_date(c))
-            else
-              db.set_string(stmt, i + 2, meta_info.get(c))
-          }
-          stmt.execute()
-        })
-      }
+      db.using_statement(db.insert_permissive(table))(stmt =>
+      {
+        db.set_string(stmt, 1, log_file.name)
+        for ((c, i) <- table.columns.tail.zipWithIndex) {
+          if (c.T == SQL.Type.Date)
+            db.set_date(stmt, i + 2, meta_info.get_date(c))
+          else
+            db.set_string(stmt, i + 2, meta_info.get(c))
+        }
+        stmt.execute()
+      })
     }
 
     def update_sessions(db: SQL.Database, log_file: Log_File)
@@ -817,33 +814,30 @@
       val build_info = log_file.parse_build_info()
       val table = Data.sessions_table
 
-      db.transaction {
-        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
-        db.using_statement(table.insert())(stmt =>
-        {
-          val entries_iterator =
-            if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
-            else build_info.sessions.iterator
-          for ((session_name, session) <- entries_iterator) {
-            db.set_string(stmt, 1, log_file.name)
-            db.set_string(stmt, 2, session_name)
-            db.set_string(stmt, 3, session.proper_chapter)
-            db.set_string(stmt, 4, session.proper_groups)
-            db.set_int(stmt, 5, session.threads)
-            db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
-            db.set_long(stmt, 7, session.timing.cpu.proper_ms)
-            db.set_long(stmt, 8, session.timing.gc.proper_ms)
-            db.set_double(stmt, 9, session.timing.factor)
-            db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
-            db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
-            db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
-            db.set_double(stmt, 13, session.ml_timing.factor)
-            db.set_long(stmt, 14, session.heap_size)
-            db.set_string(stmt, 15, session.status.map(_.toString))
-            stmt.execute()
-          }
-        })
-      }
+      db.using_statement(db.insert_permissive(table))(stmt =>
+      {
+        val entries_iterator =
+          if (build_info.sessions.isEmpty) Iterator("" -> Session_Entry.empty)
+          else build_info.sessions.iterator
+        for ((session_name, session) <- entries_iterator) {
+          db.set_string(stmt, 1, log_file.name)
+          db.set_string(stmt, 2, session_name)
+          db.set_string(stmt, 3, session.proper_chapter)
+          db.set_string(stmt, 4, session.proper_groups)
+          db.set_int(stmt, 5, session.threads)
+          db.set_long(stmt, 6, session.timing.elapsed.proper_ms)
+          db.set_long(stmt, 7, session.timing.cpu.proper_ms)
+          db.set_long(stmt, 8, session.timing.gc.proper_ms)
+          db.set_double(stmt, 9, session.timing.factor)
+          db.set_long(stmt, 10, session.ml_timing.elapsed.proper_ms)
+          db.set_long(stmt, 11, session.ml_timing.cpu.proper_ms)
+          db.set_long(stmt, 12, session.ml_timing.gc.proper_ms)
+          db.set_double(stmt, 13, session.ml_timing.factor)
+          db.set_long(stmt, 14, session.heap_size)
+          db.set_string(stmt, 15, session.status.map(_.toString))
+          stmt.execute()
+        }
+      })
     }
 
     def update_ml_statistics(db: SQL.Database, log_file: Log_File)
@@ -851,23 +845,20 @@
       val build_info = log_file.parse_build_info(ml_statistics = true)
       val table = Data.ml_statistics_table
 
-      db.transaction {
-        db.using_statement(table.delete(Data.log_name.where_equal(log_file.name)))(_.execute)
-        db.using_statement(table.insert())(stmt =>
-        {
-          val ml_stats: List[(String, Option[Bytes])] =
-            Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
-              { case (a, b) => (a, compress_properties(b.ml_statistics).proper) },
-              build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
-          val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
-          for ((session_name, ml_statistics) <- entries) {
-            db.set_string(stmt, 1, log_file.name)
-            db.set_string(stmt, 2, session_name)
-            db.set_bytes(stmt, 3, ml_statistics)
-            stmt.execute()
-          }
-        })
-      }
+      db.using_statement(db.insert_permissive(table))(stmt =>
+      {
+        val ml_stats: List[(String, Option[Bytes])] =
+          Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
+            { case (a, b) => (a, compress_properties(b.ml_statistics).proper) },
+            build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
+        val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
+        for ((session_name, ml_statistics) <- entries) {
+          db.set_string(stmt, 1, log_file.name)
+          db.set_string(stmt, 2, session_name)
+          db.set_bytes(stmt, 3, ml_statistics)
+          stmt.execute()
+        }
+      })
     }
 
     def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)

--- a/src/Pure/General/sql.scala	Wed May 03 17:00:50 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 23:04:25 2017 +0200
@@ -150,10 +150,12 @@
         (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
         ident + " " + enclosure(index_columns.map(_.name))
 
-    def insert(sql: String = ""): String =
-      "INSERT INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
+    def insert_cmd(cmd: String, sql: String = ""): String =
+      cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) +
         (if (sql == "") "" else " " + sql)
 
+    def insert(sql: String = ""): String = insert_cmd("INSERT", sql)
+
     def delete(sql: String = ""): String =
       "DELETE FROM " + ident +
         (if (sql == "") "" else " " + sql)
@@ -216,6 +218,8 @@
     def using_statement[A](sql: String)(f: PreparedStatement => A): A =
       using(statement(sql))(f)
 
+    def insert_permissive(table: Table, sql: String = ""): String
+
 
     /* input */
 
@@ -353,6 +357,9 @@
     def date(rs: ResultSet, column: SQL.Column): Date =
       date_format.parse(string(rs, column))
 
+    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+      table.insert_cmd("INSERT OR IGNORE", sql = sql)
+
     def rebuild { using_statement("VACUUM")(_.execute()) }
   }
 }
@@ -423,6 +430,10 @@
     def date(rs: ResultSet, column: SQL.Column): Date =
       Date.instant(rs.getObject(column.name, classOf[OffsetDateTime]).toInstant)
 
+    def insert_permissive(table: SQL.Table, sql: String = ""): String =
+      table.insert_cmd("INSERT",
+        sql = sql + (if (sql == "") "" else " ") + "ON CONFLICT DO NOTHING")
+
     override def close() { super.close; port_forwarding.foreach(_.close) }
   }
 }