--- a/src/Pure/General/sql.scala Sat Oct 22 19:51:08 2022 +0200
+++ b/src/Pure/General/sql.scala Sat Oct 22 20:06:55 2022 +0200
@@ -287,6 +287,8 @@
trait Database extends AutoCloseable {
db =>
+ def is_server: Boolean
+
/* types */
@@ -387,6 +389,7 @@
class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
override def toString: String = name
+ override def is_server: Boolean = false
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
@@ -461,6 +464,7 @@
port_forwarding: Option[SSH.Port_Forwarding]
) extends SQL.Database {
override def toString: String = name
+ override def is_server: Boolean = true
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_postgresql(T)
--- a/src/Pure/Thy/export.scala Sat Oct 22 19:51:08 2022 +0200
+++ b/src/Pure/Thy/export.scala Sat Oct 22 20:06:55 2022 +0200
@@ -224,8 +224,9 @@
(results, true)
})
- def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
+ def make_entry(session_name: String, args0: Protocol.Export.Args, body: Bytes): Unit = {
if (!progress.stopped && !body.is_empty) {
+ val args = if (db.is_server) args0.copy(compress = false) else args0
consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
}
}