src/Pure/General/xz.scala
author wenzelm
Mon, 03 Oct 2016 10:51:51 +0200
changeset 64002 08f89f0e8a62
parent 64000 445b3deced8f
child 64004 b4ece7a3f2ca
permissions -rw-r--r--
clarified modules; afford explicit string composition in terminate_lines;
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
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    17
  def options(): Options = options_preset(3)
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    18
08f89f0e8a62 clarified modules;
wenzelm
parents: 64000
diff changeset
    19
  def options_preset(preset: Int): 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
  }
52671
9a360530eac8 separate module XZ_File to avoid initial dependency on org.tukaani.xz;
wenzelm
parents:
diff changeset
    25
}