--- 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 */
--- 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) }
--- 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,