eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x;
authorwenzelm
Sat, 08 Jul 2023 19:32:57 +0200
changeset 78272 30d035a83dbe
parent 78271 c0dc000d2a40
child 78273 95a3bb4d7e38
child 78274 f44aec9a6894
eliminate somewhat obsolete augment_tables (see ff164add75cd), to support obsolete versions 10 and 9.x;
src/Pure/Thy/store.scala
--- a/src/Pure/Thy/store.scala	Sat Jul 08 19:28:26 2023 +0200
+++ b/src/Pure/Thy/store.scala	Sat Jul 08 19:32:57 2023 +0200
@@ -103,10 +103,6 @@
       val build_columns = List(sources, input_heaps, output_heap, return_code, uuid)
 
       val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
-
-      val augment_table: PostgreSQL.Source =
-        "ALTER TABLE IF EXISTS " + table.ident +
-        " ADD COLUMN IF NOT EXISTS " + uuid.decl(SQL.sql_type_postgresql)
     }
 
     object Sources {
@@ -429,7 +425,6 @@
       db.execute_statement(
         Store.Data.Session_Info.table.delete(
           sql = Store.Data.Session_Info.session_name.where_equal(name)))
-      if (db.is_postgresql) db.execute_statement(Store.Data.Session_Info.augment_table)
 
       db.execute_statement(Store.Data.Sources.table.delete(
         sql = Store.Data.Sources.where_equal(name)))