| author | wenzelm |
| Sun, 22 Oct 2023 12:18:23 +0200 | |
| changeset 78813 | 1829ba610c36 |
| 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 |
} |