author | wenzelm |
Wed, 12 Mar 2025 11:39:00 +0100 | |
changeset 82265 | 4b875a4c83b0 |
parent 77570 | 98b4a9902582 |
permissions | -rw-r--r-- |
77570 | 1 |
/* Title: Pure/General/zstd.scala |
76348 | 2 |
Author: Makarius |
3 |
||
4 |
Support for Zstd data compression. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
76353 | 10 |
import com.github.luben.zstd |
11 |
||
12 |
||
76348 | 13 |
object Zstd { |
76349
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
14 |
def init(): Unit = init_jni |
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
15 |
|
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
16 |
private lazy val init_jni: Unit = { |
76353 | 17 |
require(!zstd.util.Native.isLoaded(), |
76349
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
18 |
"Zstd library already initialized by other means than isabelle.Zstd.init()") |
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
19 |
|
76348 | 20 |
val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform) |
76529 | 21 |
val lib_file = File.get_file(lib_dir) |
22 |
||
23 |
System.load(lib_file.absolute_file.getPath) |
|
76349
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
wenzelm
parents:
76348
diff
changeset
|
24 |
|
76353 | 25 |
zstd.util.Native.assumeLoaded() |
26 |
assert(zstd.util.Native.isLoaded()) |
|
76348 | 27 |
Class.forName("com.github.luben.zstd.Zstd") |
28 |
} |
|
29 |
} |