tuned signature;
authorwenzelm
Thu, 04 Apr 2024 11:21:52 +0200
changeset 80082 4f9e4527a4e3
parent 80081 1ca617398213
child 80083 e2174bf626b8
tuned signature;
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)