more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;
authorwenzelm
Tue, 18 Jul 2023 12:50:34 +0200
changeset 78392 27c2fa1db6ed
parent 78391 e47233dbeab7
child 78393 a2d22d519bf2
more uniform guard (!exists_table(table)): avoid "ALTER TABLE" on already existing table, which could lead to deadlocks if this is presently locked;
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Jul 18 12:39:20 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Jul 18 12:50:34 2023 +0200
@@ -188,14 +188,13 @@
 
     def query_named: Source = query + " AS " + SQL.ident(name)
 
-    def create(strict: Boolean, sql_type: Type.Value => Source): Source = {
+    def create(sql_type: Type.Value => Source): Source = {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
           case Nil => Nil
           case keys => List("PRIMARY KEY " + enclosure(keys))
         }
-      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
+      "CREATE TABLE " + ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
     }
 
     def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
@@ -540,18 +539,20 @@
 
     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) {
-        for (column <- table.columns if column.T == SQL.Type.Bytes) {
-          execute_statement(
-            "ALTER TABLE " + table + " ALTER COLUMN " + column + " SET STORAGE EXTERNAL")
+    def create_table(table: Table, sql: Source = ""): Unit = {
+      if (!exists_table(table)) {
+        execute_statement(table.create(sql_type) + SQL.separate(sql))
+        if (is_postgresql) {
+          for (column <- table.columns if column.T == SQL.Type.Bytes) {
+            execute_statement(
+              "ALTER TABLE " + table + " ALTER COLUMN " + column + " SET STORAGE EXTERNAL")
+          }
         }
       }
     }
 
-    def create_view(table: Table, strict: Boolean = false): Unit = {
-      if (strict || !exists_table(table)) {
+    def create_view(table: Table): Unit = {
+      if (!exists_table(table)) {
         execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })
       }
     }