src/Pure/General/zstd.scala
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 77570 98b4a9902582
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
77570
98b4a9902582 tuned headers;
wenzelm
parents: 76529
diff changeset
     1
/*  Title:      Pure/General/zstd.scala
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     3
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     4
Support for Zstd data compression.
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     5
*/
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     6
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     7
package isabelle
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     8
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
     9
76353
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    10
import com.github.luben.zstd
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    11
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    12
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    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
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    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
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    20
    val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
76529
ded37aade88e clarified signature;
wenzelm
parents: 76353
diff changeset
    21
    val lib_file = File.get_file(lib_dir)
ded37aade88e clarified signature;
wenzelm
parents: 76353
diff changeset
    22
ded37aade88e clarified signature;
wenzelm
parents: 76353
diff changeset
    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
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    25
    zstd.util.Native.assumeLoaded()
3698d0f3da18 clarified signature;
wenzelm
parents: 76349
diff changeset
    26
    assert(zstd.util.Native.isLoaded())
76348
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    27
    Class.forName("com.github.luben.zstd.Zstd")
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    28
  }
a15f16e8ad18 support for Zstd data compression;
wenzelm
parents:
diff changeset
    29
}