tuned signature: more explicit operations;

--- 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 */

--- 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,