# HG changeset patch
# User wenzelm
# Date 1666350924 -7200
# Node ID b4daf7577ca0e07673e856225a8b3285350e902d
# Parent  a15f16e8ad18c8a2271099a0b97cb22e119cbb78
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;

diff -r a15f16e8ad18 -r b4daf7577ca0 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Oct 21 11:08:01 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Oct 21 13:15:24 2022 +0200
@@ -201,7 +201,7 @@
   def read_xz(path: Path): String = read_xz(path.file)
 
   def read_zstd(file: JFile): String = {
-    Zstd.init_jni
+    Zstd.init()
     read_stream(new ZstdInputStream(new BufferedInputStream(new FileInputStream(file))))
   }
   def read_zstd(path: Path): String = read_zstd(path.file)
@@ -257,7 +257,7 @@
   def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
 
   def write_zstd(file: JFile, text: String): Unit = {
-    Zstd.init_jni
+    Zstd.init()
     write_file(file, text, (s: OutputStream) => new ZstdOutputStream(new BufferedOutputStream(s)))
   }
   def write_zstd(path: Path, text: String): Unit = write_zstd(path.file, text)
diff -r a15f16e8ad18 -r b4daf7577ca0 src/Pure/General/zstd.scala
--- a/src/Pure/General/zstd.scala	Fri Oct 21 11:08:01 2022 +0200
+++ b/src/Pure/General/zstd.scala	Fri Oct 21 13:15:24 2022 +0200
@@ -8,7 +8,12 @@
 
 
 object Zstd {
-  lazy val init_jni: Unit = {
+  def init(): Unit = init_jni
+
+  private lazy val init_jni: Unit = {
+    require(!com.github.luben.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 {
@@ -16,6 +21,7 @@
         case _ => error("Exactly one file expected in directory " + lib_dir.expand)
       }
     System.load(File.platform_path(lib_file.getAbsolutePath))
+
     com.github.luben.zstd.util.Native.assumeLoaded()
     assert(com.github.luben.zstd.util.Native.isLoaded())
     Class.forName("com.github.luben.zstd.Zstd")