clarified modules;

--- a/NEWS	Sat Jun 25 10:27:42 2022 +0200
+++ b/NEWS	Sat Jun 25 13:19:15 2022 +0200
@@ -171,8 +171,8 @@
 
 * Operations for XZ compression (via Isabelle/Scala):
 
-  Isabelle_System.compress: Bytes.T -> Bytes.T
-  Isabelle_System.uncompress: Bytes.T -> Bytes.T
+  XZ.compress: Bytes.T -> Bytes.T
+  XZ.uncompress: Bytes.T -> Bytes.T
 
 
 *** System ***

--- a/etc/build.props	Sat Jun 25 10:27:42 2022 +0200
+++ b/etc/build.props	Sat Jun 25 13:19:15 2022 +0200
@@ -54,6 +54,7 @@
   src/Pure/GUI/popup.scala \
   src/Pure/GUI/wrap_panel.scala \
   src/Pure/General/antiquote.scala \
+  src/Pure/General/base64.scala \
   src/Pure/General/bytes.scala \
   src/Pure/General/cache.scala \
   src/Pure/General/codepoint.scala \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/base64.ML	Sat Jun 25 13:19:15 2022 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Pure/System/base64.ML
+    Author:     Makarius
+
+Support for Base64 data encoding (via Isabelle/Scala).
+*)
+
+signature BASE64 =
+sig
+  val decode: Bytes.T -> Bytes.T
+  val encode: Bytes.T -> Bytes.T
+end;
+
+structure Base64: BASE64 =
+struct
+
+val decode = Scala.function1_bytes "Base64.decode";
+val encode = Scala.function1_bytes "Base64.encode";
+
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/base64.scala	Sat Jun 25 13:19:15 2022 +0200
@@ -0,0 +1,26 @@
+/*  Title:      Pure/General/base64.scala
+    Author:     Makarius
+
+Support for Base64 data encoding.
+*/
+
+package isabelle
+
+
+object Base64 {
+  def encode(a: Array[Byte]): String = java.util.Base64.getEncoder.encodeToString(a)
+  def decode(s: String): Array[Byte] = java.util.Base64.getDecoder.decode(s)
+
+
+  /* Scala functions in ML */
+
+  object Decode extends Scala.Fun_Bytes("Base64.decode") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = Bytes.decode_base64(arg.text)
+  }
+
+  object Encode extends Scala.Fun_Bytes("Base64.encode") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
+  }
+}

--- a/src/Pure/General/bytes.scala	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 25 13:19:15 2022 +0200
@@ -10,7 +10,6 @@
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
 import java.net.URL
-import java.util.Base64
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
@@ -43,33 +42,10 @@
   /* base64 */
 
   def decode_base64(s: String): Bytes = {
-    val a = Base64.getDecoder.decode(s)
+    val a = Base64.decode(s)
     new Bytes(a, 0, a.length)
   }
 
-  object Decode_Base64 extends Scala.Fun_Bytes("decode_base64") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = decode_base64(arg.text)
-  }
-
-  object Encode_Base64 extends Scala.Fun_Bytes("encode_base64") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = Bytes(arg.encode_base64)
-  }
-
-
-  /* XZ compression */
-
-  object Compress extends Scala.Fun_Bytes("compress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.compress()
-  }
-
-  object Uncompress extends Scala.Fun_Bytes("uncompress") {
-    val here = Scala_Project.here
-    def apply(arg: Bytes): Bytes = arg.uncompress()
-  }
-
 
   /* read */
 
@@ -160,7 +136,7 @@
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
-    Base64.getEncoder.encodeToString(b)
+    Base64.encode(b)
   }
 
   def maybe_encode_base64: (Boolean, String) = {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xz.ML	Sat Jun 25 13:19:15 2022 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Pure/System/xz.ML
+    Author:     Makarius
+
+Support for XZ compression (via Isabelle/Scala).
+*)
+
+signature XZ =
+sig
+  val compress: Bytes.T -> Bytes.T
+  val uncompress: Bytes.T -> Bytes.T
+end;
+
+structure XZ: XZ =
+struct
+
+val compress = Scala.function1_bytes "XZ.compress";
+val uncompress = Scala.function1_bytes "XZ.uncompress";
+
+end;

--- a/src/Pure/General/xz.scala	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/General/xz.scala	Sat Jun 25 13:19:15 2022 +0200
@@ -31,4 +31,17 @@
     def apply(): ArrayCache = ArrayCache.getDefaultCache()
     def make(): ArrayCache = new BasicArrayCache
   }
+
+
+  /* Scala functions in ML */
+
+  object Compress extends Scala.Fun_Bytes("XZ.compress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.compress()
+  }
+
+  object Uncompress extends Scala.Fun_Bytes("XZ.uncompress") {
+    val here = Scala_Project.here
+    def apply(arg: Bytes): Bytes = arg.uncompress()
+  }
 }

--- a/src/Pure/ROOT.ML	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/ROOT.ML	Sat Jun 25 13:19:15 2022 +0200
@@ -300,6 +300,8 @@
 ML_file "System/scala.ML";
 ML_file "System/process_result.ML";
 ML_file "System/isabelle_system.ML";
+ML_file "General/base64.ML";
+ML_file "General/xz.ML";
 
 
 (*theory documents*)

--- a/src/Pure/System/isabelle_system.ML	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sat Jun 25 13:19:15 2022 +0200
@@ -22,10 +22,6 @@
   val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   val download: string -> Bytes.T
   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
@@ -163,18 +159,6 @@
 fun download_file url path = Bytes.write path (download url);
 
 
-(* base64 *)
-
-val decode_base64 = Scala.function1_bytes "decode_base64";
-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	Sat Jun 25 10:27:42 2022 +0200
+++ b/src/Pure/System/scala.scala	Sat Jun 25 13:19:15 2022 +0200
@@ -323,10 +323,10 @@
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
-  Bytes.Decode_Base64,
-  Bytes.Encode_Base64,
-  Bytes.Compress,
-  Bytes.Uncompress,
+  Base64.Decode,
+  Base64.Encode,
+  XZ.Compress,
+  XZ.Uncompress,
   Doc.Doc_Names,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,