# HG changeset patch
# User wenzelm
# Date 1739387142 -3600
# Node ID 18709ffb81370fc72e18c9e12261339cb113de6e
# Parent  b387a9099b7209c55f8203b70380d8357e913c5d
tuned signature: more explicit operations;

diff -r b387a9099b72 -r 18709ffb8137 src/Pure/General/file_store.scala
--- a/src/Pure/General/file_store.scala	Wed Feb 12 15:22:47 2025 +0100
+++ b/src/Pure/General/file_store.scala	Wed Feb 12 20:05:42 2025 +0100
@@ -39,15 +39,15 @@
   }
 
   def database_entry(database: Path, name: String): Option[Entry] =
-    if (!database.is_file) None
-    else {
+    if (database.is_file) {
       using(SQLite.open_database(database)) { db =>
         private_data.transaction_lock(db) {
-          if (!private_data.tables.forall(db.exists_table)) None
-          else private_data.read_entry(db, name)
+          if (private_data.tables_ok(db)) private_data.read_entry(db, name)
+          else None
         }
       }
     }
+    else None
 
 
   /* entry */
diff -r b387a9099b72 -r 18709ffb8137 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Feb 12 15:22:47 2025 +0100
+++ b/src/Pure/General/sql.scala	Wed Feb 12 20:05:42 2025 +0100
@@ -265,6 +265,9 @@
   abstract class Data(table_prefix: String = "") {
     def tables: Tables
 
+    def tables_ok(db: SQL.Database): Boolean =
+      tables.forall(db.exists_table)
+
     def transaction_lock[A](
       db: Database,
       create: Boolean = false,