isabelle: src/Pure/General/xz.scala@c5914bdd896b (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
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	}

author	wenzelm
	Fri, 06 Dec 2019 16:22:15 +0100
changeset 71252	c5914bdd896b
parent 68018	3747fe57eb67
child 71961	af779738a8f9
permissions	-rw-r--r--