# HG changeset patch
# User wenzelm
# Date 1712222512 -7200
# Node ID 4f9e4527a4e35d0f82cf2507e842d19dfb678ce2
# Parent  1ca617398213b91950730676762449c747bc7be4
tuned signature;

diff -r 1ca617398213 -r 4f9e4527a4e3 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Apr 03 16:55:34 2024 +0200
+++ b/src/Pure/General/sql.scala	Thu Apr 04 11:21:52 2024 +0200
@@ -568,6 +568,12 @@
 
     /* tables and views */
 
+    def name_pattern(name: String): String = {
+      val escape = connection.getMetaData.getSearchStringEscape
+      name.iterator.map(c =>
+        if_proper(c == '_' || c == '%' || c == escape(0), escape) + c).mkString
+    }
+
     def get_tables(pattern: String = "%"): List[String] = {
       val result = new mutable.ListBuffer[String]
       val rs = connection.getMetaData.getTables(null, null, pattern, null)
@@ -575,13 +581,8 @@
       result.toList
     }
 
-    def exists_table(name: String): Boolean = {
-      val escape = connection.getMetaData.getSearchStringEscape
-      val pattern =
-        name.iterator.map(c =>
-          if_proper(c == '_' || c == '%' || c == escape(0), escape) + c).mkString
-      get_tables(pattern = pattern).nonEmpty
-    }
+    def exists_table(name: String): Boolean =
+      get_tables(pattern = name_pattern(name)).nonEmpty
 
     def exists_table(table: Table): Boolean = exists_table(table.name)