# HG changeset patch
# User wenzelm
# Date 1688731492 -7200
# Node ID 0a7f7abbe4f08d1351ab7f3763e0cbcbfda0c584
# Parent  9d5e2a08ba1b203bef14b88ff5dd5353dd785111
more robust transaction_lock: avoid overlapping data spaces;
clarified modules;

diff -r 9d5e2a08ba1b -r 0a7f7abbe4f0 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Jul 07 10:39:28 2023 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Jul 07 14:04:52 2023 +0200
@@ -54,58 +54,77 @@
 
   /* SQL data model */
 
-  object Data {
-    val session_name = SQL.Column.string("session_name").make_primary_key
-    val name = SQL.Column.string("name").make_primary_key
-    val sources = SQL.Column.string("sources")
-    val log_xz = SQL.Column.bytes("log_xz")
-    val pdf = SQL.Column.bytes("pdf")
+  object Data extends SQL.Data("isabelle_documents") {
+    override lazy val tables = SQL.Tables(Base.table)
 
-    val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
+    object Base {
+      val session_name = SQL.Column.string("session_name").make_primary_key
+      val name = SQL.Column.string("name").make_primary_key
+      val sources = SQL.Column.string("sources")
+      val log_xz = SQL.Column.bytes("log_xz")
+      val pdf = SQL.Column.bytes("pdf")
+
+      val table = make_table("", List(session_name, name, sources, log_xz, pdf))
+    }
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       SQL.where_and(
-        Data.session_name.equal(session_name),
-        if_proper(name, Data.name.equal(name)))
+        Base.session_name.equal(session_name),
+        if_proper(name, Base.name.equal(name)))
+
+    def clean_session(db: SQL.Database, session_name: String): Unit =
+      db.execute_statement(Base.table.delete(sql = Base.session_name.where_equal(session_name)))
+
+    def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
+      db.execute_query_statement(
+        Base.table.select(List(Base.name, Base.sources), sql = where_equal(session_name)),
+        List.from[Document_Input],
+        { res =>
+          val name = res.string(Base.name)
+          val sources = res.string(Base.sources)
+          Document_Input(name, SHA1.fake_shasum(sources))
+        }
+      )
+
+    def read_document(
+      db: SQL.Database,
+      session_name: String,
+      name: String
+    ): Option[Document_Output] = {
+      db.execute_query_statementO[Document_Output](
+        Base.table.select(sql = where_equal(session_name, name = name)),
+        { res =>
+          val name = res.string(Base.name)
+          val sources = res.string(Base.sources)
+          val log_xz = res.bytes(Base.log_xz)
+          val pdf = res.bytes(Base.pdf)
+          Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
+        }
+      )
+    }
+
+    def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
+      db.execute_statement(Base.table.insert(), body =
+        { stmt =>
+          stmt.string(1) = session_name
+          stmt.string(2) = doc.name
+          stmt.string(3) = doc.sources.toString
+          stmt.bytes(4) = doc.log_xz
+          stmt.bytes(5) = doc.pdf
+        })
   }
 
+  def clean_session(db: SQL.Database, session_name: String): Unit =
+    Data.transaction_lock(db, create = true) { Data.clean_session(db, session_name) }
+
   def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
-    db.execute_query_statement(
-      Data.table.select(List(Data.name, Data.sources), sql = Data.where_equal(session_name)),
-      List.from[Document_Input],
-      { res =>
-        val name = res.string(Data.name)
-        val sources = res.string(Data.sources)
-        Document_Input(name, SHA1.fake_shasum(sources))
-      }
-    )
+    Data.transaction_lock(db) { Data.read_documents(db, session_name) }
 
-  def read_document(
-    db: SQL.Database,
-    session_name: String,
-    name: String
-  ): Option[Document_Output] = {
-    db.execute_query_statementO[Document_Output](
-      Data.table.select(sql = Data.where_equal(session_name, name)),
-      { res =>
-        val name = res.string(Data.name)
-        val sources = res.string(Data.sources)
-        val log_xz = res.bytes(Data.log_xz)
-        val pdf = res.bytes(Data.pdf)
-        Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf)
-      }
-    )
-  }
+  def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
+    Data.transaction_lock(db) { Data.read_document(db, session_name, name) }
 
   def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
-    db.execute_statement(Data.table.insert(), body =
-      { stmt =>
-        stmt.string(1) = session_name
-        stmt.string(2) = doc.name
-        stmt.string(3) = doc.sources.toString
-        stmt.bytes(4) = doc.log_xz
-        stmt.bytes(5) = doc.pdf
-      })
+    Data.transaction_lock(db) { Data.write_document(db, session_name, doc) }
 
 
   /* background context */
diff -r 9d5e2a08ba1b -r 0a7f7abbe4f0 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Jul 07 10:39:28 2023 +0200
+++ b/src/Pure/Thy/export.scala	Fri Jul 07 14:04:52 2023 +0200
@@ -51,6 +51,9 @@
         if_proper(theory_name, Base.theory_name.equal(theory_name)),
         if_proper(name, Base.name.equal(name)))
 
+    def clean_session(db: SQL.Database, session_name: String): Unit =
+      db.execute_statement(Base.table.delete(sql = where_equal(session_name)))
+
     def readable_entry(db: SQL.Database, entry_name: Entry_Name): Boolean = {
       db.execute_query_statementB(
         Base.table.select(List(Base.name),
@@ -200,6 +203,9 @@
     (entry_name: Entry_Name) => regs.exists(_.matches(entry_name.compound_name))
   }
 
+  def clean_session(db: SQL.Database, session_name: String): Unit =
+    Data.transaction_lock(db, create = true) { Data.clean_session(db, session_name) }
+
   def read_theory_names(db: SQL.Database, session_name: String): List[String] =
     Data.transaction_lock(db) { Data.read_theory_names(db, session_name) }
 
diff -r 9d5e2a08ba1b -r 0a7f7abbe4f0 src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Fri Jul 07 10:39:28 2023 +0200
+++ b/src/Pure/Thy/store.scala	Fri Jul 07 14:04:52 2023 +0200
@@ -78,9 +78,7 @@
   /* SQL data model */
 
   object Data extends SQL.Data() {
-    override lazy val tables =
-      SQL.Tables(Session_Info.table, Sources.table,
-        Export.Data.Base.table, Document_Build.Data.table)
+    override lazy val tables = SQL.Tables(Session_Info.table, Sources.table)
 
     object Session_Info {
       val session_name = SQL.Column.string("session_name").make_primary_key
@@ -134,7 +132,7 @@
       build_log: Build_Log.Session_Info,
       build: Build_Info
     ): Unit = {
-      db.execute_statement(Store.Data.Session_Info.table.insert(), body =
+      db.execute_statement(Data.Session_Info.table.insert(), body =
         { stmt =>
           stmt.string(1) = session_name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
@@ -386,7 +384,10 @@
       Store.Data.Session_Info.table.select(List(Store.Data.Session_Info.session_name),
         sql = Store.Data.Session_Info.session_name.where_equal(name)))
 
-  def clean_session_info(db: SQL.Database, name: String): Boolean =
+  def clean_session_info(db: SQL.Database, name: String): Boolean = {
+    Export.clean_session(db, name)
+    Document_Build.clean_session(db, name)
+
     Store.Data.transaction_lock(db, create = true, synchronized = true) {
       val already_defined = session_info_defined(db, name)
 
@@ -398,14 +399,9 @@
       db.execute_statement(Store.Data.Sources.table.delete(
         sql = Store.Data.Sources.where_equal(name)))
 
-      db.execute_statement(
-        Export.Data.Base.table.delete(sql = Export.Data.Base.session_name.where_equal(name)))
-
-      db.execute_statement(
-        Document_Build.Data.table.delete(sql = Document_Build.Data.session_name.where_equal(name)))
-
       already_defined
     }
+  }
 
   def write_session_info(
     db: SQL.Database,