--- a/src/Pure/Admin/build_log.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Admin/build_log.scala Sun Mar 10 10:50:12 2024 +0100
@@ -689,6 +689,13 @@
object private_data extends SQL.Data("isabelle_build_log") {
/* tables */
+ override lazy val tables: SQL.Tables =
+ SQL.Tables(
+ meta_info_table,
+ sessions_table,
+ theories_table,
+ ml_statistics_table)
+
val meta_info_table =
make_table(Column.log_name :: Prop.all_props ::: Settings.all_settings, name = "meta_info")
@@ -711,13 +718,6 @@
make_table(List(Column.log_name, Column.session_name, Column.ml_statistics),
name = "ml_statistics")
- override val tables: SQL.Tables =
- SQL.Tables(
- meta_info_table,
- sessions_table,
- theories_table,
- ml_statistics_table)
-
/* earliest pull date for repository version (PostgreSQL queries) */
--- a/src/Pure/Build/build_process.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Build/build_process.scala Sun Mar 10 10:50:12 2024 +0100
@@ -287,6 +287,16 @@
object private_data extends SQL.Data("isabelle_build") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+ override lazy val tables: SQL.Tables =
+ SQL.Tables(
+ Updates.table,
+ Sessions.table,
+ Pending.table,
+ Running.table,
+ Results.table,
+ Base.table,
+ Workers.table)
+
def pull[A <: Library.Named](
data_domain: Set[String],
data_iterator: Set[String] => Iterator[A],
@@ -840,16 +850,6 @@
/* collective operations */
- override val tables: SQL.Tables =
- SQL.Tables(
- Updates.table,
- Sessions.table,
- Pending.table,
- Running.table,
- Results.table,
- Base.table,
- Workers.table)
-
private val build_uuid_tables =
tables.filter(table =>
table.columns.exists(column => column.name == Generic.build_uuid.name))
--- a/src/Pure/Build/build_schedule.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Sun Mar 10 10:50:12 2024 +0100
@@ -1061,6 +1061,12 @@
object private_data extends SQL.Data("isabelle_build") {
import Build_Process.private_data.{Base, Generic}
+ override lazy val tables: SQL.Tables =
+ SQL.Tables(Schedules.table, Nodes.table)
+
+ lazy val all_tables: SQL.Tables =
+ SQL.Tables.list(Build_Process.private_data.tables.list ::: tables.list)
+
/* schedule */
@@ -1211,11 +1217,6 @@
remove_schedules(db, update.delete)
}
-
- override val tables: SQL.Tables = SQL.Tables(Schedules.table, Nodes.table)
-
- val all_tables: SQL.Tables =
- SQL.Tables.list(Build_Process.private_data.tables.list ::: tables.list)
}
--- a/src/Pure/Build/export.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Build/export.scala Sun Mar 10 10:50:12 2024 +0100
@@ -31,7 +31,7 @@
/* SQL data model */
object private_data extends SQL.Data() {
- override lazy val tables = SQL.Tables(Base.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Base.table)
object Base {
val session_name = SQL.Column.string("session_name").make_primary_key
--- a/src/Pure/Build/store.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Build/store.scala Sun Mar 10 10:50:12 2024 +0100
@@ -114,7 +114,7 @@
/* SQL data model */
object private_data extends SQL.Data() {
- override lazy val tables = SQL.Tables(Session_Info.table, Sources.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Session_Info.table, Sources.table)
object Session_Info {
val session_name = SQL.Column.string("session_name").make_primary_key
--- a/src/Pure/ML/ml_heap.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala Sun Mar 10 10:50:12 2024 +0100
@@ -41,7 +41,7 @@
sealed case class Log_DB(uuid: String, content: Bytes)
object private_data extends SQL.Data("isabelle_heaps") {
- override lazy val tables = SQL.Tables(Base.table, Slices.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Base.table, Slices.table)
object Generic {
val name = SQL.Column.string("name").make_primary_key
--- a/src/Pure/System/host.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/System/host.scala Sun Mar 10 10:50:12 2024 +0100
@@ -168,7 +168,7 @@
object private_data extends SQL.Data("isabelle_host") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/host.db")
- override lazy val tables = SQL.Tables(Node_Info.table, Info.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Node_Info.table, Info.table)
object Node_Info {
val hostname = SQL.Column.string("hostname").make_primary_key
--- a/src/Pure/System/progress.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/System/progress.scala Sun Mar 10 10:50:12 2024 +0100
@@ -56,7 +56,8 @@
object private_data extends SQL.Data("isabelle_progress") {
val database: Path = Path.explode("$ISABELLE_HOME_USER/progress.db")
- override lazy val tables = SQL.Tables(Base.table, Agents.table, Messages.table)
+ override lazy val tables: SQL.Tables =
+ SQL.Tables(Base.table, Agents.table, Messages.table)
object Base {
val context_uuid = SQL.Column.string("context_uuid").make_primary_key
--- a/src/Pure/Thy/document_build.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Thy/document_build.scala Sun Mar 10 10:50:12 2024 +0100
@@ -55,7 +55,7 @@
/* SQL data model */
object private_data extends SQL.Data("isabelle_documents") {
- override lazy val tables = SQL.Tables(Base.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Base.table)
object Base {
val session_name = SQL.Column.string("session_name").make_primary_key
--- a/src/Pure/Tools/server.scala Sun Mar 10 10:40:48 2024 +0100
+++ b/src/Pure/Tools/server.scala Sun Mar 10 10:50:12 2024 +0100
@@ -366,7 +366,7 @@
object private_data extends SQL.Data() {
val database = Path.explode("$ISABELLE_HOME_USER/servers.db")
- override lazy val tables = SQL.Tables(Base.table)
+ override lazy val tables: SQL.Tables = SQL.Tables(Base.table)
object Base {
val name = SQL.Column.string("name").make_primary_key