# HG changeset patch
# User wenzelm
# Date 1712223645 -7200
# Node ID e2174bf626b8e39e68bde82b84c96abad48ae61a
# Parent  4f9e4527a4e35d0f82cf2507e842d19dfb678ce2
more portable: prefer official JDBC operation DatabaseMetaData.getColumns();

diff -r 4f9e4527a4e3 -r e2174bf626b8 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Apr 04 11:21:52 2024 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu Apr 04 11:40:45 2024 +0200
@@ -1044,13 +1044,9 @@
       db.transaction {
         val upgrade_table = private_data.sessions_table
         val upgrade_column = Column.session_start
-        val upgrade = {
+        val upgrade =
           db.exists_table(upgrade_table) &&
-          !db.execute_query_statementB(
-            "SELECT NULL as result FROM information_schema.columns " +
-            " WHERE table_name = " + SQL.string(upgrade_table.name) +
-            " AND column_name = " + SQL.string(upgrade_column.name))
-        }
+          !db.exists_table_column(upgrade_table, upgrade_column)
 
         private_data.tables.lock(db, create = true)
 
diff -r 4f9e4527a4e3 -r e2174bf626b8 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Apr 04 11:21:52 2024 +0200
+++ b/src/Pure/General/sql.scala	Thu Apr 04 11:40:45 2024 +0200
@@ -581,11 +581,28 @@
       result.toList
     }
 
+    def get_table_columns(
+      table_pattern: String = "%",
+      pattern: String = "%"
+    ): List[(String, String)] = {
+      val result = new mutable.ListBuffer[(String, String)]
+      val rs = connection.getMetaData.getColumns(null, null, table_pattern, pattern)
+      while (rs.next) { result += (rs.getString(3) -> rs.getString(4)) }
+      result.toList
+    }
+
     def exists_table(name: String): Boolean =
       get_tables(pattern = name_pattern(name)).nonEmpty
 
     def exists_table(table: Table): Boolean = exists_table(table.name)
 
+    def exists_table_column(table_name: String, name: String): Boolean =
+      get_table_columns(table_pattern = name_pattern(table_name), pattern = name_pattern(name))
+        .nonEmpty
+
+    def exists_table_column(table: Table, column: Column): Boolean =
+      exists_table_column(table.name, column.name)
+
     def create_table(table: Table, sql: Source = ""): Unit = {
       if (!exists_table(table)) {
         execute_statement(table.create(sql_type) + SQL.separate(sql))