# 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)