# HG changeset patch
# User wenzelm
# Date 1710064212 -3600
# Node ID ac40138234ce4b169978331756a7d1c2fcbc2074
# Parent  c052a35e6a4f23852f1f3f67bec9cf733308ec6d
tuned signature: more uniform SQL.Data instances;

diff -r c052a35e6a4f -r ac40138234ce src/Pure/Admin/build_log.scala
--- 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) */
 
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Build/build_process.scala
--- 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))
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Build/build_schedule.scala
--- 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)
   }
 
 
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Build/export.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Build/store.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/ML/ml_heap.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/System/host.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/System/progress.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Thy/document_build.scala
--- 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
diff -r c052a35e6a4f -r ac40138234ce src/Pure/Tools/server.scala
--- 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