clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
authorwenzelm
Fri, 21 Oct 2022 13:15:24 +0200
changeset 76349 b4daf7577ca0
parent 76348 a15f16e8ad18
child 76350 978f7ca3329f
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
src/Pure/General/file.scala
src/Pure/General/zstd.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)
--- 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")