isabelle: src/Pure/General/xz.scala@83d1f210a1d3 (annotated)

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	}

author	wenzelm
	Sat, 04 Mar 2017 08:41:32 +0100
changeset 65100	83d1f210a1d3
parent 64004	b4ece7a3f2ca
child 68018	3747fe57eb67
permissions	-rw-r--r--