src/Pure/General/xz.scala
author wenzelm
Thu, 09 Jun 2022 21:28:15 +0200
changeset 75547 460a25031ccd
parent 75393 87ebf5a50283
child 75620 44815dc2b8f9
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64000
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
     1
/*  Title:      Pure/General/xz.scala
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     3
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
     4
Support for XZ data compression.
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     5
*/
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     6
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     7
package isabelle
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     8
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
     9
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    10
import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache}
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    11
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    12
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73024
diff changeset
    13
object XZ {
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    14
  /* options */
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    15
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    16
  type Options = LZMA2Options
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    17
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73024
diff changeset
    18
  def options(preset: Int = 3): Options = {
64000
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    19
    val opts = new LZMA2Options
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    20
    opts.setPreset(preset)
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    21
    opts
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    22
  }
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    23
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    24
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    25
  /* cache */
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    26
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    27
  type Cache = ArrayCache
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    28
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 73024
diff changeset
    29
  object Cache {
73024
337e1b135d2f clarified signature --- internal Cache.none;
wenzelm
parents: 71961
diff changeset
    30
    def none: ArrayCache = ArrayCache.getDummyCache()
337e1b135d2f clarified signature --- internal Cache.none;
wenzelm
parents: 71961
diff changeset
    31
    def apply(): ArrayCache = ArrayCache.getDefaultCache()
337e1b135d2f clarified signature --- internal Cache.none;
wenzelm
parents: 71961
diff changeset
    32
    def make(): ArrayCache = new BasicArrayCache
337e1b135d2f clarified signature --- internal Cache.none;
wenzelm
parents: 71961
diff changeset
    33
  }
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    34
}