back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
authorwenzelm
Thu, 16 Mar 2023 16:28:21 +0100 (23 months ago)
changeset 77681 1db732e6c3d2
parent 77680 bc8e2fec9650
child 77682 a76f49a03448
back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
src/Pure/General/sql.scala
src/Pure/Thy/export.scala
--- a/src/Pure/General/sql.scala	Thu Mar 16 16:13:58 2023 +0100
+++ b/src/Pure/General/sql.scala	Thu Mar 16 16:28:21 2023 +0100
@@ -442,8 +442,15 @@
       result.toList
     }
 
-    def create_table(table: Table, strict: Boolean = false, sql: Source = ""): Unit =
+    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_index(table: Table, name: String, columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Unit =
--- a/src/Pure/Thy/export.scala	Thu Mar 16 16:13:58 2023 +0100
+++ b/src/Pure/Thy/export.scala	Thu Mar 16 16:28:21 2023 +0100
@@ -235,9 +235,8 @@
             (results, true)
           })
 
-    def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
+    def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
-        val args = if (db.is_postgresql) args0.copy(compress = false) else args0
         consumer.send(Entry.make(session_name, args, body, cache) -> args.strict)
       }
     }