# HG changeset patch # User wenzelm # Date 1666368392 -7200 # Node ID 3698d0f3da18f910d9e286a9795653bd3d02b841 # Parent f2b98eb6a7a9612b0970d7b67e8ff0dc5420fd89 clarified signature; diff -r f2b98eb6a7a9 -r 3698d0f3da18 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Fri Oct 21 17:56:56 2022 +0200 +++ b/src/Pure/General/bytes.scala Fri Oct 21 18:06:32 2022 +0200 @@ -7,11 +7,10 @@ package isabelle -import com.github.luben.zstd.{ZstdInputStream, ZstdOutputStream} - import java.io.{ByteArrayInputStream, ByteArrayOutputStream, FileInputStream, FileOutputStream, InputStream, OutputStream, File as JFile} import java.net.URL -import org.tukaani.xz.{XZInputStream, XZOutputStream} +import org.tukaani.xz +import com.github.luben.zstd object Bytes { @@ -214,8 +213,11 @@ def uncompress(cache: Compress.Cache = Compress.Cache.none): Bytes = using( - if (detect_xz) new XZInputStream(stream(), cache.xz) - else if (detect_zstd) { Zstd.init(); new ZstdInputStream(stream(), cache.zstd) } + if (detect_xz) new xz.XZInputStream(stream(), cache.for_xz) + else if (detect_zstd) { + Zstd.init() + new zstd.ZstdInputStream(stream(), cache.for_zstd) + } else detect_error() )(Bytes.read_stream(_, hint = length)) @@ -233,10 +235,10 @@ using( options match { case options_xz: Compress.Options_XZ => - new XZOutputStream(result, options_xz.make, cache.xz) + new xz.XZOutputStream(result, options_xz.make, cache.for_xz) case options_zstd: Compress.Options_Zstd => Zstd.init() - new ZstdOutputStream(result, cache.zstd, options_zstd.level) + new zstd.ZstdOutputStream(result, cache.for_zstd, options_zstd.level) })(write_stream) new Bytes(result.toByteArray, 0, result.size) } diff -r f2b98eb6a7a9 -r 3698d0f3da18 src/Pure/General/compress.scala --- a/src/Pure/General/compress.scala Fri Oct 21 17:56:56 2022 +0200 +++ b/src/Pure/General/compress.scala Fri Oct 21 18:06:32 2022 +0200 @@ -7,9 +7,8 @@ package isabelle -import org.tukaani.xz.{LZMA2Options, ArrayCache, BasicArrayCache} -import com.github.luben.zstd.{BufferPool, NoPool, RecyclingBufferPool, - ZstdInputStream, ZstdOutputStream} +import org.tukaani.xz +import com.github.luben.zstd object Compress { @@ -20,8 +19,8 @@ } sealed abstract class Options case class Options_XZ(level: Int = 3) extends Options { - def make: LZMA2Options = { - val opts = new LZMA2Options + def make: xz.LZMA2Options = { + val opts = new xz.LZMA2Options opts.setPreset(level) opts } @@ -31,14 +30,17 @@ /* cache */ - class Cache private(val xz: ArrayCache, val zstd: BufferPool) + class Cache private(val for_xz: xz.ArrayCache, val for_zstd: zstd.BufferPool) object Cache { - def none: Cache = { Zstd.init(); new Cache(ArrayCache.getDummyCache(), NoPool.INSTANCE) } + def none: Cache = { + Zstd.init() + new Cache(xz.ArrayCache.getDummyCache(), zstd.NoPool.INSTANCE) + } def make(): Cache = { Zstd.init() - val pool = Untyped.constructor(classOf[RecyclingBufferPool]).newInstance() - new Cache(new BasicArrayCache, pool) + val pool = Untyped.constructor(classOf[zstd.RecyclingBufferPool]).newInstance() + new Cache(new xz.BasicArrayCache, pool) } } diff -r f2b98eb6a7a9 -r 3698d0f3da18 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Fri Oct 21 17:56:56 2022 +0200 +++ b/src/Pure/General/file.scala Fri Oct 21 18:06:32 2022 +0200 @@ -17,9 +17,8 @@ import java.util.zip.{GZIPInputStream, GZIPOutputStream} import java.util.EnumSet -import org.tukaani.xz.{XZInputStream, XZOutputStream} - -import com.github.luben.zstd.{ZstdInputStream, ZstdOutputStream} +import org.tukaani.xz +import com.github.luben.zstd import scala.collection.mutable @@ -197,12 +196,12 @@ def read_gzip(path: Path): String = read_gzip(path.file) def read_xz(file: JFile): String = - read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file)))) + read_stream(new xz.XZInputStream(new BufferedInputStream(new FileInputStream(file)))) def read_xz(path: Path): String = read_xz(path.file) def read_zstd(file: JFile): String = { Zstd.init() - read_stream(new ZstdInputStream(new BufferedInputStream(new FileInputStream(file)))) + read_stream(new zstd.ZstdInputStream(new BufferedInputStream(new FileInputStream(file)))) } def read_zstd(path: Path): String = read_zstd(path.file) @@ -250,7 +249,8 @@ def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text) def write_xz(file: JFile, text: String, options: Compress.Options_XZ): Unit = - File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options.make)) + File.write_file(file, text, + s => new xz.XZOutputStream(new BufferedOutputStream(s), options.make)) def write_xz(file: JFile, text: String): Unit = write_xz(file, text, Compress.Options_XZ()) def write_xz(path: Path, text: String, options: Compress.Options_XZ): Unit = write_xz(path.file, text, options) @@ -258,7 +258,8 @@ def write_zstd(file: JFile, text: String, options: Compress.Options_Zstd): Unit = { Zstd.init() - File.write_file(file, text, s => new ZstdOutputStream(new BufferedOutputStream(s), options.level)) + File.write_file(file, text, + s => new zstd.ZstdOutputStream(new BufferedOutputStream(s), options.level)) } def write_zstd(file: JFile, text: String): Unit = write_zstd(file, text, Compress.Options_Zstd()) diff -r f2b98eb6a7a9 -r 3698d0f3da18 src/Pure/General/zstd.scala --- a/src/Pure/General/zstd.scala Fri Oct 21 17:56:56 2022 +0200 +++ b/src/Pure/General/zstd.scala Fri Oct 21 18:06:32 2022 +0200 @@ -7,11 +7,14 @@ package isabelle +import com.github.luben.zstd + + object Zstd { def init(): Unit = init_jni private lazy val init_jni: Unit = { - require(!com.github.luben.zstd.util.Native.isLoaded(), + require(!zstd.util.Native.isLoaded(), "Zstd library already initialized by other means than isabelle.Zstd.init()") val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform) @@ -22,8 +25,8 @@ } System.load(File.platform_path(lib_file.getAbsolutePath)) - com.github.luben.zstd.util.Native.assumeLoaded() - assert(com.github.luben.zstd.util.Native.isLoaded()) + zstd.util.Native.assumeLoaded() + assert(zstd.util.Native.isLoaded()) Class.forName("com.github.luben.zstd.Zstd") } }