clarified signature: more specific exists_table --- avoid retrieving full list beforehand;
--- a/src/Pure/General/sql.scala Mon Jul 17 11:39:32 2023 +0200
+++ b/src/Pure/General/sql.scala Mon Jul 17 12:15:06 2023 +0200
@@ -536,13 +536,23 @@
/* tables and views */
- def tables: List[String] = {
+ def get_tables(pattern: String = "%"): List[String] = {
val result = new mutable.ListBuffer[String]
- val rs = connection.getMetaData.getTables(null, null, "%", null)
+ val rs = connection.getMetaData.getTables(null, null, pattern, null)
while (rs.next) { result += rs.getString(3) }
result.toList
}
+ def exists_table(name: String): Boolean = {
+ val escape = connection.getMetaData.getSearchStringEscape
+ val pattern =
+ name.iterator.map(c =>
+ (if (c == '_' || c == '%' || c == escape(0)) escape else "") + c).mkString
+ get_tables(pattern = pattern).nonEmpty
+ }
+
+ def exists_table(table: Table): Boolean = exists_table(table.name)
+
def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit = {
execute_statement(table.create(strict, sql_type) + SQL.separate(sql))
if (is_postgresql) {
@@ -558,7 +568,7 @@
execute_statement(table.create_index(name, columns, strict, unique))
def create_view(table: Table, strict: Boolean = false): Unit = {
- if (strict || !tables.contains(table.name)) {
+ if (strict || exists_table(table)) {
execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })
}
}
--- a/src/Pure/Thy/store.scala Mon Jul 17 11:39:32 2023 +0200
+++ b/src/Pure/Thy/store.scala Mon Jul 17 12:15:06 2023 +0200
@@ -150,7 +150,7 @@
Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = {
- if (db.tables.contains(Session_Info.table.name)) {
+ if (db.exists_table(Session_Info.table)) {
db.execute_query_statementO[Store.Build_Info](
Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)),
{ res =>
@@ -421,10 +421,8 @@
/* session info */
- def session_info_exists(db: SQL.Database): Boolean = {
- val tables = db.tables
- Store.Data.tables.forall(table => tables.contains(table.name))
- }
+ def session_info_exists(db: SQL.Database): Boolean =
+ Store.Data.tables.forall(db.exists_table)
def session_info_defined(db: SQL.Database, name: String): Boolean =
db.execute_query_statementB(
--- a/src/Pure/Tools/server.scala Mon Jul 17 11:39:32 2023 +0200
+++ b/src/Pure/Tools/server.scala Mon Jul 17 12:15:06 2023 +0200
@@ -375,7 +375,7 @@
}
def list(db: SQLite.Database): List[Info] =
- if (db.tables.contains(Data.table.name)) {
+ if (db.exists_table(Data.table)) {
db.execute_query_statement(Data.table.select(),
List.from[Info],
{ res =>