clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
--- 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")