--- 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 =
--- 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" "";
--- 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,