# HG changeset patch # User wenzelm # Date 1655846846 -7200 # Node ID 3362b6a5d6974089a4bc1ce400be35ab483ecee0 # Parent d3ba143a7ab8244cb0ccb7a218b0f10165008803 support XZ compression in Isabelle/ML; diff -r d3ba143a7ab8 -r 3362b6a5d697 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Tue Jun 21 23:05:37 2022 +0200 +++ b/src/Pure/General/bytes.scala Tue Jun 21 23:27:26 2022 +0200 @@ -60,6 +60,21 @@ } + /* XZ compression */ + + object Compress extends Scala.Fun("compress") { + val here = Scala_Project.here + def invoke(args: List[Bytes]): List[Bytes] = + List(Library.the_single(args).compress()) + } + + object Uncompress extends Scala.Fun("uncompress") { + val here = Scala_Project.here + def invoke(args: List[Bytes]): List[Bytes] = + List(Library.the_single(args).uncompress()) + } + + /* read */ def read_stream(stream: InputStream, limit: Int = Integer.MAX_VALUE, hint: Int = 1024): Bytes = diff -r d3ba143a7ab8 -r 3362b6a5d697 src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML Tue Jun 21 23:05:37 2022 +0200 +++ b/src/Pure/System/isabelle_system.ML Tue Jun 21 23:27:26 2022 +0200 @@ -24,6 +24,8 @@ val download_file: string -> Path.T -> unit val decode_base64: Bytes.T -> Bytes.T val encode_base64: Bytes.T -> Bytes.T + val compress: Bytes.T -> Bytes.T + val uncompress: Bytes.T -> Bytes.T val isabelle_id: unit -> string val isabelle_identifier: unit -> string option val isabelle_heading: unit -> string @@ -167,6 +169,12 @@ val encode_base64 = Scala.function1_bytes "encode_base64"; +(* XZ compression *) + +val compress = Scala.function1_bytes "compress"; +val uncompress = Scala.function1_bytes "uncompress"; + + (* Isabelle distribution identification *) fun isabelle_id () = Scala.function1 "isabelle_id" ""; diff -r d3ba143a7ab8 -r 3362b6a5d697 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Tue Jun 21 23:05:37 2022 +0200 +++ b/src/Pure/System/scala.scala Tue Jun 21 23:27:26 2022 +0200 @@ -309,6 +309,8 @@ Scala.Toplevel, Bytes.Decode_Base64, Bytes.Encode_Base64, + Bytes.Compress, + Bytes.Uncompress, Doc.Doc_Names, Bibtex.Check_Database, Isabelle_System.Make_Directory,