support XZ compression in Isabelle/ML;
authorwenzelm
Tue, 21 Jun 2022 23:27:26 +0200
changeset 75579 3362b6a5d697
parent 75578 d3ba143a7ab8
child 75580 5c1c4f537ae8
support XZ compression in Isabelle/ML;
src/Pure/General/bytes.scala
src/Pure/System/isabelle_system.ML
src/Pure/System/scala.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 =
--- 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,