| author | wenzelm | 
| Wed, 16 Oct 2024 21:41:05 +0200 | |
| changeset 81177 | 137ea3d464be | 
| 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: 
76348diff
changeset | 14 | def init(): Unit = init_jni | 
| 
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
 wenzelm parents: 
76348diff
changeset | 15 | |
| 
b4daf7577ca0
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
 wenzelm parents: 
76348diff
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: 
76348diff
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: 
76348diff
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: 
76348diff
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 | } |