| author | wenzelm | 
| Thu, 15 Feb 2024 13:00:56 +0100 | |
| changeset 79622 | e413c94b192a | 
| 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  | 
}  |