back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g. relevant for old_command_timings_blob, but also for prospective heaps;
--- 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)
}
}