# HG changeset patch
# User desharna
# Date 1666457268 -7200
# Node ID 2b204e11141c2dfa27cba434a30a78ab254adc5b
# Parent  f7002e5b15bbb345cc935f2ee3a9ce8040b0b202# Parent  cff0828c374f721991aff33734c4b25d18612a08
merged

diff -r f7002e5b15bb -r 2b204e11141c Admin/components/components.sha1
--- a/Admin/components/components.sha1	Thu Oct 20 14:43:29 2022 +0200
+++ b/Admin/components/components.sha1	Sat Oct 22 18:47:48 2022 +0200
@@ -158,6 +158,7 @@
 056979bd1c08eb9d0d12cc1118b4ff70bfe2d594 isabelle_setup-20220701.tar.gz
 be91402b3e5ef5bc6d4802a45175ee238cd9653e isabelle_setup-20220808.tar.gz
 171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz
+7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -515,3 +516,4 @@
 b884c60653002a7811e3b652ae0515e825d98667 zipperposition-2.0.tar.gz
 b129ec4f8a4474953ec107536298ee08a01fbebc zipperposition-2.1-1.tar.gz
 5f53a77efb5cbe9d0c95d74a1588cc923bd711a7 zipperposition-2.1.tar.gz
+c101182780aeafbc2e0ea7e8b10b91c6f7483af2 zstd-jni-1.5.2-5.tar.gz
diff -r f7002e5b15bb -r 2b204e11141c Admin/components/main
--- a/Admin/components/main	Thu Oct 20 14:43:29 2022 +0200
+++ b/Admin/components/main	Sat Oct 22 18:47:48 2022 +0200
@@ -9,7 +9,7 @@
 flatlaf-2.4
 idea-icons-20210508
 isabelle_fonts-20211004
-isabelle_setup-20220817
+isabelle_setup-20221020
 jdk-17.0.4.1+1
 jedit-20211103
 jfreechart-1.5.3
@@ -34,3 +34,4 @@
 xz-java-1.9
 z3-4.4.0_4.4.1
 zipperposition-2.1-1
+zstd-jni-1.5.2-5
diff -r f7002e5b15bb -r 2b204e11141c NEWS
--- a/NEWS	Thu Oct 20 14:43:29 2022 +0200
+++ b/NEWS	Sat Oct 22 18:47:48 2022 +0200
@@ -50,6 +50,22 @@
   - Added lemma wfP_subset_mset[simp].
 
 
+*** ML ***
+
+* Operations for Zstd compression (via Isabelle/Scala):
+
+  Zstd.compress: Bytes.T -> Bytes.T
+  Zstd.uncompress: Bytes.T -> Bytes.T
+
+
+*** System ***
+
+* Isabelle/Scala provides generic support for XZ and Zstd compression,
+via Compress.Options and Compress.Cache. Bytes.uncompress automatically
+detects the compression scheme.
+
+
+
 New in Isabelle2022 (October 2022)
 ----------------------------------
 
diff -r f7002e5b15bb -r 2b204e11141c bin/isabelle_java
--- a/bin/isabelle_java	Thu Oct 20 14:43:29 2022 +0200
+++ b/bin/isabelle_java	Sat Oct 22 18:47:48 2022 +0200
@@ -64,7 +64,7 @@
     exit 127
   else
     unset ISABELLE_HOME
-    unset CLASSPATH
+    export CLASSPATH=""
     exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
       -classpath "$ISABELLE_CLASSPATH" "$@"
   fi
diff -r f7002e5b15bb -r 2b204e11141c etc/build.props
--- a/etc/build.props	Thu Oct 20 14:43:29 2022 +0200
+++ b/etc/build.props	Sat Oct 22 18:47:48 2022 +0200
@@ -34,6 +34,7 @@
   src/Pure/Admin/build_vampire.scala \
   src/Pure/Admin/build_verit.scala \
   src/Pure/Admin/build_zipperposition.scala \
+  src/Pure/Admin/build_zstd.scala \
   src/Pure/Admin/check_sources.scala \
   src/Pure/Admin/ci_build.scala \
   src/Pure/Admin/isabelle_cronjob.scala \
@@ -62,6 +63,7 @@
   src/Pure/General/codepoint.scala \
   src/Pure/General/comment.scala \
   src/Pure/General/completion.scala \
+  src/Pure/General/compress.scala \
   src/Pure/General/csv.scala \
   src/Pure/General/date.scala \
   src/Pure/General/exn.scala \
@@ -99,7 +101,7 @@
   src/Pure/General/uuid.scala \
   src/Pure/General/value.scala \
   src/Pure/General/word.scala \
-  src/Pure/General/xz.scala \
+  src/Pure/General/zstd.scala \
   src/Pure/Isar/document_structure.scala \
   src/Pure/Isar/keyword.scala \
   src/Pure/Isar/line_structure.scala \
diff -r f7002e5b15bb -r 2b204e11141c lib/Tools/java
--- a/lib/Tools/java	Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/java	Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
 eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
 
 classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
 
 isabelle_java java "${JAVA_ARGS[@]}" \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r f7002e5b15bb -r 2b204e11141c lib/Tools/scala
--- a/lib/Tools/scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scala	Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
 isabelle scala_build || exit $?
 
 classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
 
 export jvm_cp_args="$(platform_path "$ISABELLE_CLASSPATH")"
 export JAVA_OPTS="$ISABELLE_JAVA_SYSTEM_OPTIONS -J-Dscala.usejavacp=true"
diff -r f7002e5b15bb -r 2b204e11141c lib/Tools/scala_build
--- a/lib/Tools/scala_build	Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scala_build	Sat Oct 22 18:47:48 2022 +0200
@@ -57,7 +57,7 @@
   "$ISABELLE_HOME/lib/classes/Pure.shasum" \
   "$ISABELLE_HOME/src/Tools/jEdit/dist"
 
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 
diff -r f7002e5b15bb -r 2b204e11141c lib/Tools/scalac
--- a/lib/Tools/scalac	Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/Tools/scalac	Sat Oct 22 18:47:48 2022 +0200
@@ -7,7 +7,7 @@
 isabelle scala_build || exit $?
 
 classpath "$ISABELLE_SETUP_CLASSPATH"; unset ISABELLE_SETUP_CLASSPATH
-classpath "$CLASSPATH"; unset CLASSPATH
+classpath "$CLASSPATH"; export CLASSPATH=""
 
 isabelle_scala scalac -Dfile.encoding=UTF-8 \
   -classpath "$(platform_path "$ISABELLE_CLASSPATH")" "$@"
diff -r f7002e5b15bb -r 2b204e11141c lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Oct 20 14:43:29 2022 +0200
+++ b/lib/scripts/getsettings	Sat Oct 22 18:47:48 2022 +0200
@@ -41,7 +41,7 @@
   ISABELLE_ROOT="$(platform_path "$ISABELLE_HOME")"
 
   ISABELLE_CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
-  unset CLASSPATH
+  export CLASSPATH=""
 else
   if [ -z "$USER_HOME" ]; then
     USER_HOME="$HOME"
@@ -50,7 +50,7 @@
   ISABELLE_ROOT="$ISABELLE_HOME"
 
   ISABELLE_CLASSPATH="$CLASSPATH"
-  unset CLASSPATH
+  export CLASSPATH=""
 fi
 
 #init cumulative settings
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -359,7 +359,7 @@
           session_build_info :::
           ml_statistics.map(Protocol.ML_Statistics_Marker.apply) :::
           session_errors.map(Protocol.Error_Message_Marker.apply) :::
-          heap_sizes), XZ.options(6))
+          heap_sizes), Compress.Options_XZ(6))
 
 
       /* next build */
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -616,7 +616,10 @@
       errors = log_file.filter(Protocol.Error_Message_Marker))
   }
 
-  def compress_errors(errors: List[String], cache: XZ.Cache = XZ.Cache()): Option[Bytes] =
+  def compress_errors(
+    errors: List[String],
+    cache: Compress.Cache = Compress.Cache.none
+  ): Option[Bytes] =
     if (errors.isEmpty) None
     else {
       Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
@@ -627,7 +630,7 @@
     if (bytes.is_empty) Nil
     else {
       XML.Decode.list(YXML.string_of_body)(
-        YXML.parse_body(bytes.uncompress(cache = cache.xz).text, cache = cache))
+        YXML.parse_body(bytes.uncompress(cache = cache.compress).text, cache = cache))
     }
 
 
@@ -954,7 +957,7 @@
           stmt.double(13) = session.ml_timing.factor
           stmt.long(14) = session.heap_size
           stmt.string(15) = session.status.map(_.toString)
-          stmt.bytes(16) = compress_errors(session.errors, cache = cache.xz)
+          stmt.bytes(16) = compress_errors(session.errors, cache = cache.compress)
           stmt.string(17) = session.sources
           stmt.execute()
         }
@@ -988,7 +991,7 @@
       db.using_statement(db.insert_permissive(table)) { stmt =>
         val ml_stats: List[(String, Option[Bytes])] =
           Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
-            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.xz).proper) },
+            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = cache.compress).proper) },
             build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
         val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
         for ((session_name, ml_statistics) <- entries) {
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Admin/build_zstd.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_zstd.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,119 @@
+/*  Title:      Pure/Admin/build_zstd.scala
+    Author:     Makarius
+
+Build Isabelle zstd-jni component from official download.
+*/
+
+package isabelle
+
+
+object Build_Zstd {
+  /* platforms */
+
+  sealed case class Platform(name: String, template: String, exe: Boolean = false) {
+    def install(jar_dir: Path, component_dir: Path, version: String): Unit = {
+      val source = jar_dir + Path.explode(template.replace("{V}", version))
+      val target = Isabelle_System.make_directory(component_dir + Path.basic(name))
+      Isabelle_System.copy_file(source, target)
+      if (exe) File.set_executable(target + source.base, true)
+    }
+  }
+
+  private val platforms =
+    List(
+      Platform("arm64-darwin", "darwin/aarch64/libzstd-jni-{V}.dylib"),
+      Platform("x86_64-darwin", "darwin/x86_64/libzstd-jni-{V}.dylib"),
+      Platform("arm64-linux", "linux/aarch64/libzstd-jni-{V}.so"),
+      Platform("x86_64-linux", "linux/amd64/libzstd-jni-{V}.so"),
+      Platform("x86_64-windows", "win/amd64/libzstd-jni-{V}.dll", exe = true))
+
+
+  /* build zstd */
+
+  val license_url = "https://raw.githubusercontent.com/luben/zstd-jni/master/LICENSE"
+  val default_download_url = "https://repo1.maven.org/maven2/com/github/luben/zstd-jni"
+  val default_version = "1.5.2-5"
+
+  def build_zstd(
+    target_dir: Path = Path.current,
+    download_url: String = default_download_url,
+    version: String = default_version,
+    progress: Progress = new Progress,
+  ): Unit = {
+    /* component */
+
+    val component_name = "zstd-jni-" + version
+    val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
+    progress.echo("Component " + component_dir)
+
+    File.write(component_dir + Path.basic("README"),
+      "This is " + component_name + " from\n" + download_url +
+        "\n\n        Makarius\n        " + Date.Format.date(Date.now()) + "\n")
+
+    Isabelle_System.download_file(
+      license_url, component_dir + Path.basic("LICENSE"), progress = progress)
+
+
+    /* jar */
+
+    val jar_name = component_name + ".jar"
+    val jar = component_dir + Path.basic(jar_name)
+    Isabelle_System.download_file(
+      download_url + "/" + version + "/" + jar_name, jar, progress = progress)
+
+    Isabelle_System.with_tmp_dir("build") { jar_dir =>
+      progress.echo("Unpacking " + jar)
+      Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
+        cwd = jar_dir.file).check
+      for (platform <- platforms) platform.install(jar_dir, component_dir, version)
+    }
+
+
+    /* settings */
+
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+
+    File.write(etc_dir + Path.basic("settings"),
+"""# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_ZSTD_HOME="$COMPONENT"
+
+classpath "$ISABELLE_ZSTD_HOME/""" + jar_name + """"
+""")
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_zstd", "build Isabelle zstd-jni component from official download",
+      Scala_Project.here,
+      { args =>
+        var target_dir = Path.current
+        var download_url = default_download_url
+        var version = default_version
+
+        val getopts = Getopts("""
+Usage: isabelle build_zstd [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """ + quote(default_download_url) + """)
+    -V VERSION   version (default: """ + quote(default_version) + """)
+
+  Build zstd-jni component from the specified download base URL and VERSION,
+  see also https://github.com/luben/zstd-jni
+""",
+          "D:" -> (arg => target_dir = Path.explode(arg)),
+          "U:" -> (arg => download_url = arg),
+          "V:" -> (arg => version = arg))
+
+        val more_args = getopts(args)
+        if (more_args.nonEmpty) getopts.usage()
+
+        val progress = new Console_Progress()
+
+        build_zstd(target_dir = target_dir, download_url = download_url,
+          version = version, progress = progress)
+      })
+}
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Admin/jenkins.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -112,7 +112,7 @@
         File.write_xz(log_path,
           terminate_lines(Url.read(main_log) ::
             ml_statistics.map(Protocol.ML_Statistics_Marker.apply)),
-          XZ.options(6))
+          Compress.Options_XZ(6))
       }
     }
   }
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/bytes.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -7,11 +7,10 @@
 package isabelle
 
 
-import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
-  OutputStream, InputStream, FileInputStream, FileOutputStream}
+import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream, InputStream, OutputStream, File as JFile}
 import java.net.URL
-
-import org.tukaani.xz.{XZInputStream, XZOutputStream}
+import org.tukaani.xz
+import com.github.luben.zstd
 
 
 object Bytes {
@@ -191,20 +190,61 @@
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
-  /* XZ data compression */
+  /* XZ / Zstd data compression */
 
-  def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
-    using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
+  def detect_xz: Boolean =
+    length >= 6 &&
+      bytes(offset)     == 0xFD.toByte &&
+      bytes(offset + 1) == 0x37.toByte &&
+      bytes(offset + 2) == 0x7A.toByte &&
+      bytes(offset + 3) == 0x58.toByte &&
+      bytes(offset + 4) == 0x5A.toByte &&
+      bytes(offset + 5) == 0x00.toByte
+
+  def detect_zstd: Boolean =
+    length >= 4 &&
+      bytes(offset)     == 0x28.toByte &&
+      bytes(offset + 1) == 0xB5.toByte &&
+      bytes(offset + 2) == 0x2F.toByte &&
+      bytes(offset + 3) == 0xFD.toByte
+
+  def uncompress_xz(cache: Compress.Cache = Compress.Cache.none): Bytes =
+    using(new xz.XZInputStream(stream(), cache.for_xz))(Bytes.read_stream(_, hint = length))
 
-  def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = {
-    val result = new ByteArrayOutputStream(length)
-    using(new XZOutputStream(result, options, cache))(write_stream(_))
-    new Bytes(result.toByteArray, 0, result.size)
+  def uncompress_zstd(cache: Compress.Cache = Compress.Cache.none): Bytes = {
+    Zstd.init()
+    val n = zstd.Zstd.decompressedSize(bytes, offset, length)
+    if (n > 0 && n < Integer.MAX_VALUE) {
+      Bytes(zstd.Zstd.decompress(array, n.toInt))
+    }
+    else {
+      using(new zstd.ZstdInputStream(stream(), cache.for_zstd))(Bytes.read_stream(_, hint = length))
+    }
+  }
+
+  def uncompress(cache: Compress.Cache = Compress.Cache.none): Bytes =
+    if (detect_xz) uncompress_xz(cache = cache)
+    else if (detect_zstd) uncompress_zstd(cache = cache)
+    else error("Cannot detect compression scheme")
+
+  def compress(
+    options: Compress.Options = Compress.Options(),
+    cache: Compress.Cache = Compress.Cache.none
+  ): Bytes = {
+    options match {
+      case options_xz: Compress.Options_XZ =>
+        val result = new ByteArrayOutputStream(length)
+        using(new xz.XZOutputStream(result, options_xz.make, cache.for_xz))(write_stream)
+        new Bytes(result.toByteArray, 0, result.size)
+      case options_zstd: Compress.Options_Zstd =>
+        Zstd.init()
+        Bytes(zstd.Zstd.compress(array, options_zstd.level))
+    }
   }
 
   def maybe_compress(
-    options: XZ.Options = XZ.options(),
-    cache: XZ.Cache = XZ.Cache()
+    options: Compress.Options = Compress.Options(),
+    cache: Compress.Cache = Compress.Cache.none
   ) : (Boolean, Bytes) = {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/compress.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/compress.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,69 @@
+/*  Title:      Pure/General/compress.scala
+    Author:     Makarius
+
+Support for generic data compression.
+*/
+
+package isabelle
+
+
+import org.tukaani.xz
+import com.github.luben.zstd
+
+
+object Compress {
+  /* options */
+
+  object Options {
+    def apply(): Options = Options_XZ()
+  }
+  sealed abstract class Options
+  case class Options_XZ(level: Int = 3) extends Options {
+    def make: xz.LZMA2Options = {
+      val opts = new xz.LZMA2Options
+      opts.setPreset(level)
+      opts
+    }
+  }
+  case class Options_Zstd(level: Int = 3) extends Options
+
+
+  /* cache */
+
+  class Cache private(val for_xz: xz.ArrayCache, val for_zstd: zstd.BufferPool)
+
+  object Cache {
+    def none: Cache = {
+      Zstd.init()
+      new Cache(xz.ArrayCache.getDummyCache(), zstd.NoPool.INSTANCE)
+  }
+    def make(): Cache = {
+      Zstd.init()
+      val pool = Untyped.constructor(classOf[zstd.RecyclingBufferPool]).newInstance()
+      new Cache(new xz.BasicArrayCache, pool)
+    }
+  }
+
+
+  /* Scala functions in ML */
+
+  object XZ_Compress extends Scala.Fun_Bytes("XZ.compress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.compress(Options_XZ())
+  }
+
+  object XZ_Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.uncompress_xz()
+  }
+
+  object Zstd_Compress extends Scala.Fun_Bytes("Zstd.compress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.compress(Options_Zstd())
+  }
+
+  object Zstd_Uncompress extends Scala.Fun_Bytes("Zstd.uncompress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.uncompress_zstd()
+  }
+}
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/file.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -17,7 +17,8 @@
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.EnumSet
 
-import org.tukaani.xz.{XZInputStream, XZOutputStream}
+import org.tukaani.xz
+import com.github.luben.zstd
 
 import scala.collection.mutable
 
@@ -85,6 +86,7 @@
   def is_thy(s: String): Boolean = s.endsWith(".thy")
   def is_xz(s: String): Boolean = s.endsWith(".xz")
   def is_zip(s: String): Boolean = s.endsWith(".zip")
+  def is_zst(s: String): Boolean = s.endsWith(".zst")
 
   def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig")
 
@@ -194,9 +196,15 @@
   def read_gzip(path: Path): String = read_gzip(path.file)
 
   def read_xz(file: JFile): String =
-    read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
+    read_stream(new xz.XZInputStream(new BufferedInputStream(new FileInputStream(file))))
   def read_xz(path: Path): String = read_xz(path.file)
 
+  def read_zstd(file: JFile): String = {
+    Zstd.init()
+    read_stream(new zstd.ZstdInputStream(new BufferedInputStream(new FileInputStream(file))))
+  }
+  def read_zstd(path: Path): String = read_zstd(path.file)
+
 
   /* read lines */
 
@@ -240,12 +248,25 @@
     write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
   def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text)
 
-  def write_xz(file: JFile, text: String, options: XZ.Options): Unit =
-    File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
-  def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options())
-  def write_xz(path: Path, text: String, options: XZ.Options): Unit =
+  def write_xz(file: JFile, text: String, options: Compress.Options_XZ): Unit =
+    File.write_file(file, text,
+      s => new xz.XZOutputStream(new BufferedOutputStream(s), options.make))
+  def write_xz(file: JFile, text: String): Unit = write_xz(file, text, Compress.Options_XZ())
+  def write_xz(path: Path, text: String, options: Compress.Options_XZ): Unit =
     write_xz(path.file, text, options)
-  def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
+  def write_xz(path: Path, text: String): Unit = write_xz(path, text, Compress.Options_XZ())
+
+  def write_zstd(file: JFile, text: String, options: Compress.Options_Zstd): Unit = {
+    Zstd.init()
+    File.write_file(file, text,
+      s => new zstd.ZstdOutputStream(new BufferedOutputStream(s), options.level))
+  }
+  def write_zstd(file: JFile, text: String): Unit =
+    write_zstd(file, text, Compress.Options_Zstd())
+  def write_zstd(path: Path, text: String, options: Compress.Options_Zstd): Unit =
+    write_zstd(path.file, text, options)
+  def write_zstd(path: Path, text: String): Unit =
+    write_zstd(path, text, Compress.Options_Zstd())
 
   def write_backup(path: Path, text: String): Unit = {
     if (path.is_file) Isabelle_System.move_file(path, path.backup)
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/http.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -22,7 +22,7 @@
     val mime_type_html: String = "text/html; charset=utf-8"
 
     val default_mime_type: String = mime_type_bytes
-    val default_encoding: String = UTF8.charset_name
+    val default_encoding: String = UTF8.charset.name
 
     def apply(
         bytes: Bytes,
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/path.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -240,6 +240,7 @@
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")
   def shasum: Path = ext("shasum")
+  def zst: Path = ext("zst")
 
   def backup: Path = {
     val (prfx, s) = split_path
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/properties.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -54,8 +54,8 @@
   }
 
   def compress(ps: List[T],
-    options: XZ.Options = XZ.options(),
-    cache: XZ.Cache = XZ.Cache()
+    options: Compress.Options = Compress.Options(),
+    cache: Compress.Cache = Compress.Cache.none
   ): Bytes = {
     if (ps.isEmpty) Bytes.empty
     else {
@@ -69,7 +69,7 @@
     else {
       val ps =
         XML.Decode.list(XML.Decode.properties)(
-          YXML.parse_body(bs.uncompress(cache = cache.xz).text))
+          YXML.parse_body(bs.uncompress(cache = cache.compress).text))
       if (cache.no_cache) ps else ps.map(cache.props)
     }
   }
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/url.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -64,8 +64,8 @@
 
   /* strings */
 
-  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
-  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
+  def decode(s: String): String = URLDecoder.decode(s, UTF8.charset)
+  def encode(s: String): String = URLEncoder.encode(s, UTF8.charset)
 
 
   /* read */
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/utf8.scala
--- a/src/Pure/General/utf8.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/General/utf8.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -7,16 +7,13 @@
 package isabelle
 
 
-import java.nio.charset.Charset
-import scala.io.Codec
+import java.nio.charset.{Charset, StandardCharsets}
 
 
 object UTF8 {
   /* charset */
 
-  val charset_name: String = "UTF-8"
-  val charset: Charset = Charset.forName(charset_name)
-  def codec(): Codec = Codec(charset)
+  val charset: Charset = StandardCharsets.UTF_8
 
   def bytes(s: String): Array[Byte] = s.getBytes(charset)
 
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/xz.scala
--- a/src/Pure/General/xz.scala	Thu Oct 20 14:43:29 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-/*  Title:      Pure/General/xz.scala
-    Author:     Makarius
-
-Support for XZ data compression.
-*/
-
-package isabelle
-
-
-import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache}
-
-
-object XZ {
-  /* options */
-
-  type Options = LZMA2Options
-
-  def options(preset: Int = 3): Options = {
-    val opts = new LZMA2Options
-    opts.setPreset(preset)
-    opts
-  }
-
-
-  /* cache */
-
-  type Cache = ArrayCache
-
-  object Cache {
-    def none: ArrayCache = ArrayCache.getDummyCache()
-    def apply(): ArrayCache = ArrayCache.getDefaultCache()
-    def make(): ArrayCache = new BasicArrayCache
-  }
-
-
-  /* Scala functions in ML */
-
-  object Compress extends Scala.Fun_Bytes("XZ.compress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.compress()
-  }
-
-  object Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.uncompress()
-  }
-}
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/zstd.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/zstd.ML	Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Pure/General/zstd.ML
+    Author:     Makarius
+
+Support for Zstd compression (via Isabelle/Scala).
+*)
+
+signature Zstd =
+sig
+  val compress: Bytes.T -> Bytes.T
+  val uncompress: Bytes.T -> Bytes.T
+end;
+
+structure Zstd: Zstd =
+struct
+
+val compress = \<^scala>\<open>Zstd.compress\<close>;
+val uncompress = \<^scala>\<open>Zstd.uncompress\<close>;
+
+end;
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/General/zstd.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/zstd.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Pure/General/xz.scala
+    Author:     Makarius
+
+Support for Zstd data compression.
+*/
+
+package isabelle
+
+
+import com.github.luben.zstd
+
+
+object Zstd {
+  def init(): Unit = init_jni
+
+  private lazy val init_jni: Unit = {
+    require(!zstd.util.Native.isLoaded(),
+      "Zstd library already initialized by other means than isabelle.Zstd.init()")
+
+    val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
+    val lib_file =
+      File.find_files(lib_dir.file) match {
+        case List(file) => file
+        case _ => error("Exactly one file expected in directory " + lib_dir.expand)
+      }
+    System.load(File.platform_path(lib_file.getAbsolutePath))
+
+    zstd.util.Native.assumeLoaded()
+    assert(zstd.util.Native.isLoaded())
+    Class.forName("com.github.luben.zstd.Zstd")
+  }
+}
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/PIDE/xml.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -189,15 +189,15 @@
 
   object Cache {
     def make(
-        xz: XZ.Cache = XZ.Cache.make(),
+        compress: Compress.Cache = Compress.Cache.make(),
         max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
-      new Cache(xz, max_string, initial_size)
+      new Cache(compress, max_string, initial_size)
 
-    val none: Cache = make(XZ.Cache.none, max_string = 0)
+    val none: Cache = make(Compress.Cache.none, max_string = 0)
   }
 
-  class Cache(val xz: XZ.Cache, max_string: Int, initial_size: Int)
+  class Cache(val compress: Compress.Cache, max_string: Int, initial_size: Int)
   extends isabelle.Cache(max_string, initial_size) {
     protected def cache_props(x: Properties.T): Properties.T = {
       if (x.isEmpty) x
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/ROOT.ML	Sat Oct 22 18:47:48 2022 +0200
@@ -348,6 +348,7 @@
 
 ML_file "General/base64.ML";
 ML_file "General/xz.ML";
+ML_file "General/zstd.ML";
 ML_file "Tools/build.ML";
 ML_file "Tools/named_thms.ML";
 ML_file "Tools/print_operation.ML";
@@ -364,4 +365,3 @@
 ML_file "Tools/jedit.ML";
 ML_file "Tools/ghc.ML";
 ML_file "Tools/generated_files.ML";
-
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/System/isabelle_charset.scala
--- a/src/Pure/System/isabelle_charset.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/isabelle_charset.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -22,7 +22,7 @@
 
 class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) {
   override def contains(cs: Charset): Boolean =
-    cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs)
+    cs.name.equalsIgnoreCase(UTF8.charset.name) || UTF8.charset.contains(cs)
 
   override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder
 
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -175,6 +175,7 @@
   Build_Vampire.isabelle_tool,
   Build_VeriT.isabelle_tool,
   Build_Zipperposition.isabelle_tool,
+  Build_Zstd.isabelle_tool,
   Check_Sources.isabelle_tool,
   Components.isabelle_tool,
   isabelle.vscode.Build_VSCode.isabelle_tool,
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/System/scala.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -368,8 +368,10 @@
   Scala_Build.Scala_Fun,
   Base64.Decode,
   Base64.Encode,
-  XZ.Compress,
-  XZ.Uncompress,
+  Compress.XZ_Compress,
+  Compress.XZ_Uncompress,
+  Compress.Zstd_Compress,
+  Compress.Zstd_Uncompress,
   Doc.Doc_Names,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -134,7 +134,7 @@
 
     def uncompressed: Bytes = {
       val (compressed, bytes) = body.join
-      if (compressed) bytes.uncompress(cache = cache.xz) else bytes
+      if (compressed) bytes.uncompress(cache = cache.compress) else bytes
     }
 
     def uncompressed_yxml: XML.Body =
@@ -183,7 +183,7 @@
     cache: XML.Cache
   ): Entry = {
     val body =
-      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
+      if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.compress))
       else Future.value((false, bytes))
     val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
     Entry(entry_name, args.executable, body, cache)
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -1149,6 +1149,7 @@
             info_roots += make_info(chapter_defs, options, select, dir, chapter, entry)
           case _ =>
         }
+        chapter = UNSORTED
       }
       info_roots.toList
     }
@@ -1487,11 +1488,11 @@
         db.using_statement(table.insert()) { stmt =>
           stmt.string(1) = name
           stmt.bytes(2) = Properties.encode(build_log.session_timing)
-          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.xz)
-          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.xz)
-          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.xz)
-          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.xz)
-          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.xz)
+          stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache.compress)
+          stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache.compress)
+          stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress)
+          stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress)
+          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress)
           stmt.string(8) = build.sources
           stmt.string(9) = cat_lines(build.input_heaps)
           stmt.string(10) = build.output_heap getOrElse ""
diff -r f7002e5b15bb -r 2b204e11141c src/Pure/term.scala
--- a/src/Pure/term.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Pure/term.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -177,16 +177,16 @@
 
   object Cache {
     def make(
-        xz: XZ.Cache = XZ.Cache.make(),
+        compress: Compress.Cache = Compress.Cache.make(),
         max_string: Int = isabelle.Cache.default_max_string,
         initial_size: Int = isabelle.Cache.default_initial_size): Cache =
-      new Cache(xz, initial_size, max_string)
+      new Cache(compress, initial_size, max_string)
 
     val none: Cache = make(max_string = 0)
   }
 
-  class Cache(xz: XZ.Cache, max_string: Int, initial_size: Int)
-  extends XML.Cache(xz, max_string, initial_size) {
+  class Cache(compress: Compress.Cache, max_string: Int, initial_size: Int)
+  extends XML.Cache(compress, max_string, initial_size) {
     protected def cache_indexname(x: Indexname): Indexname =
       lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index))
 
diff -r f7002e5b15bb -r 2b204e11141c src/Tools/Setup/src/Environment.java
--- a/src/Tools/Setup/src/Environment.java	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/Setup/src/Environment.java	Sat Oct 22 18:47:48 2022 +0200
@@ -9,6 +9,7 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.util.HashMap;
@@ -179,6 +180,11 @@
 
     /* raw process */
 
+    private static read_file(path: Path): String =
+    {
+        return new String(Files.readAllBytes(path), StandardCharsets.UTF_8);
+    }
+
     public static ProcessBuilder process_builder(
         List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
     {
@@ -242,8 +248,8 @@
             }
 
             int rc = proc.exitValue();
-            String out = Files.readString(out_file);
-            String err = Files.readString(err_file);
+            String out = read_file(out_file);
+            String err = read_file(err_file);
             res = new Exec_Result(rc, out, err);
         }
         finally {
@@ -388,7 +394,7 @@
                 Exec_Result res = exec_process(cmd, null, env, true);
                 if (!res.ok()) throw new RuntimeException(res.out());
 
-                for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+                for (String s : read_file(settings_file).split("\u0000", -1)) {
                     int i = s.indexOf('=');
                     if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
                     else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
diff -r f7002e5b15bb -r 2b204e11141c src/Tools/jEdit/src/isabelle_encoding.scala
--- a/src/Tools/jEdit/src/isabelle_encoding.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -40,10 +40,10 @@
   }
 
   override def getTextReader(in: InputStream): Reader =
-    text_reader(in, UTF8.codec(), true)
+    text_reader(in, Codec(UTF8.charset), true)
 
   override def getPermissiveTextReader(in: InputStream): Reader = {
-    val codec = UTF8.codec()
+    val codec = Codec(UTF8.charset)
     codec.onMalformedInput(CodingErrorAction.REPLACE)
     codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
     text_reader(in, codec, false)
@@ -52,7 +52,7 @@
   override def getTextWriter(out: OutputStream): Writer = {
     val buffer = new ByteArrayOutputStream(BUFSIZE) {
       override def flush(): Unit = {
-        val text = Symbol.encode(toString(UTF8.charset_name))
+        val text = Symbol.encode(toString(UTF8.charset))
         out.write(UTF8.bytes(text))
         out.flush()
       }
diff -r f7002e5b15bb -r 2b204e11141c src/Tools/jEdit/src/jedit_main.scala
--- a/src/Tools/jEdit/src/jedit_main.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_main.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -128,7 +128,7 @@
         catch {
           case exn: Throwable =>
             GUI.init_laf()
-            GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+            GUI.dialog(null, "Isabelle main", GUI.scrollable_text(Exn.print(exn)))
             sys.exit(Process_Result.RC.failure)
         }
       }
diff -r f7002e5b15bb -r 2b204e11141c src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Thu Oct 20 14:43:29 2022 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sat Oct 22 18:47:48 2022 +0200
@@ -29,7 +29,7 @@
       }
       catch {
         case exn: Throwable =>
-          GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+          GUI.dialog(view, "Isabelle build", GUI.scrollable_text(Exn.print(exn)))
       }
     }
   }