src/Pure/General/xz.scala
author wenzelm
Fri, 20 Apr 2018 22:17:42 +0200
changeset 68018 3747fe57eb67
parent 64004 b4ece7a3f2ca
child 71961 af779738a8f9
permissions -rw-r--r--
support for XZ.Cache;
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
64000
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    13
object XZ
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    14
{
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    15
  /* options */
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    16
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    17
  type Options = LZMA2Options
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    18
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64002
diff changeset
    19
  def options(preset: Int = 3): Options =
64000
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    20
  {
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    21
    val opts = new LZMA2Options
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    22
    opts.setPreset(preset)
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    23
    opts
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    24
  }
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    25
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    26
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    27
  /* cache */
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    28
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    29
  type Cache = ArrayCache
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    30
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    31
  def cache(): ArrayCache = ArrayCache.getDefaultCache()
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 64004
diff changeset
    32
  def make_cache(): ArrayCache = new BasicArrayCache
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    33
}