src/Pure/General/xz.scala
author wenzelm
Sun, 21 May 2017 23:41:46 +0200
changeset 65895 744878d72021
parent 64004 b4ece7a3f2ca
child 68018 3747fe57eb67
permissions -rw-r--r--
more general workaround for failed sessions (again, see also 2edb89630a80, ed7b5cd3a7f2);
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
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    10
import org.tukaani.xz.LZMA2Options
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
{
64002
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    15
  type Options = LZMA2Options
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    16
64004
b4ece7a3f2ca clarified stream operations;
wenzelm
parents: 64002
diff changeset
    17
  def options(preset: Int = 3): Options =
64000
445b3deced8f clarified modules;
wenzelm
parents: 52671
diff changeset
    18
  {
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
  }
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    23
}