# HG changeset patch
# User wenzelm
# Date 1666462536 -7200
# Node ID 2c0f252fb11cc009e5e582241efe492e8f30aaf1
# Parent  2b204e11141c2dfa27cba434a30a78ab254adc5b# Parent  f7174238b5e3cf015c252fd4f200711ed672bfc9
merged

diff -r 2b204e11141c -r 2c0f252fb11c src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sat Oct 22 18:47:48 2022 +0200
+++ b/src/Pure/General/bytes.scala	Sat Oct 22 20:15:36 2022 +0200
@@ -238,7 +238,7 @@
         new Bytes(result.toByteArray, 0, result.size)
       case options_zstd: Compress.Options_Zstd =>
         Zstd.init()
-        Bytes(zstd.Zstd.compress(array, options_zstd.level))
+        Bytes(zstd.Zstd.compress(if (offset == 0) bytes else array, options_zstd.level))
     }
   }
 
diff -r 2b204e11141c -r 2c0f252fb11c src/Pure/General/compress.scala
--- a/src/Pure/General/compress.scala	Sat Oct 22 18:47:48 2022 +0200
+++ b/src/Pure/General/compress.scala	Sat Oct 22 20:15:36 2022 +0200
@@ -15,7 +15,7 @@
   /* options */
 
   object Options {
-    def apply(): Options = Options_XZ()
+    def apply(): Options = Options_Zstd()
   }
   sealed abstract class Options
   case class Options_XZ(level: Int = 3) extends Options {
diff -r 2b204e11141c -r 2c0f252fb11c src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat Oct 22 18:47:48 2022 +0200
+++ b/src/Pure/General/sql.scala	Sat Oct 22 20:15:36 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)
 
diff -r 2b204e11141c -r 2c0f252fb11c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Oct 22 18:47:48 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Oct 22 20:15:36 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)
       }
     }