diff --git a/src/Pure/General/bytes.scala b/src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala
+++ b/src/Pure/General/bytes.scala
@@ -1,220 +1,235 @@
 /*  Title:      Pure/General/bytes.scala
     Author:     Makarius
 
 Immutable byte vectors versus UTF8 strings.
 */
 
 package isabelle
 
 
 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}
 
 
 object Bytes {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
   def apply(s: CharSequence): Bytes = {
     val str = s.toString
     if (str.isEmpty) empty
     else {
       val b = UTF8.bytes(str)
       new Bytes(b, 0, b.length)
     }
   }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)
 
   def apply(a: Array[Byte], offset: Int, length: Int): Bytes =
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
       System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
   val newline: Bytes = apply("\n")
 
 
   /* base64 */
 
   def base64(s: String): Bytes = {
     val a = Base64.getDecoder.decode(s)
     new Bytes(a, 0, a.length)
   }
 
   object Decode_Base64 extends Scala.Fun("decode_base64") {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(base64(Library.the_single(args).text))
   }
 
   object Encode_Base64 extends Scala.Fun("encode_base64") {
     val here = Scala_Project.here
     def invoke(args: List[Bytes]): List[Bytes] =
       List(Bytes(Library.the_single(args).base64))
   }
 
 
+  /* 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 =
     if (limit == 0) empty
     else {
       val out_size = (if (limit == Integer.MAX_VALUE) hint else limit) max 1024
       val out = new ByteArrayOutputStream(out_size)
       val buf = new Array[Byte](8192)
       var m = 0
 
       var cont = true
       while (cont) {
         m = stream.read(buf, 0, buf.length min (limit - out.size))
         if (m != -1) out.write(buf, 0, m)
         cont = (m != -1 && limit > out.size)
       }
 
       new Bytes(out.toByteArray, 0, out.size)
     }
 
   def read(file: JFile): Bytes = {
     val length = file.length
     val limit = if (length < 0 || length > Integer.MAX_VALUE) Integer.MAX_VALUE else length.toInt
     using(new FileInputStream(file))(read_stream(_, limit = limit))
   }
 
   def read(path: Path): Bytes = read(path.file)
 
   def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
 
 
   /* write */
 
   def write(file: JFile, bytes: Bytes): Unit =
     using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }
 
 final class Bytes private(
   protected val bytes: Array[Byte],
   protected val offset: Int,
   val length: Int) extends CharSequence {
   /* equality */
 
   override def equals(that: Any): Boolean = {
     that match {
       case other: Bytes =>
         if (this eq other) true
         else if (length != other.length) false
         else (0 until length).forall(i => bytes(offset + i) == other.bytes(other.offset + i))
       case _ => false
     }
   }
 
   private lazy val hash: Int = {
     var h = 0
     for (i <- offset until offset + length) {
       val b = bytes(i).asInstanceOf[Int] & 0xFF
       h = 31 * h + b
     }
     h
   }
 
   override def hashCode(): Int = hash
 
 
   /* content */
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   def is_empty: Boolean = length == 0
 
   def iterator: Iterator[Byte] =
     for (i <- (offset until (offset + length)).iterator)
       yield bytes(i)
 
   def array: Array[Byte] = {
     val a = new Array[Byte](length)
     System.arraycopy(bytes, offset, a, 0, length)
     a
   }
 
   def text: String = UTF8.decode_permissive(this)
 
   def base64: String = {
     val b =
       if (offset == 0 && length == bytes.length) bytes
       else Bytes(bytes, offset, length).bytes
     Base64.getEncoder.encodeToString(b)
   }
 
   def maybe_base64: (Boolean, String) = {
     val s = text
     if (this == Bytes(s)) (false, s) else (true, base64)
   }
 
   override def toString: String = "Bytes(" + length + ")"
 
   def proper: Option[Bytes] = if (is_empty) None else Some(this)
   def proper_text: Option[String] = if (is_empty) None else Some(text)
 
   def +(other: Bytes): Bytes =
     if (other.is_empty) this
     else if (is_empty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
       System.arraycopy(bytes, offset, new_bytes, 0, length)
       System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }
 
 
   /* CharSequence operations */
 
   def charAt(i: Int): Char =
     if (0 <= i && i < length) (bytes(offset + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
     else throw new IndexOutOfBoundsException
 
   def subSequence(i: Int, j: Int): Bytes = {
     if (0 <= i && i <= j && j <= length) new Bytes(bytes, offset + i, j - i)
     else throw new IndexOutOfBoundsException
   }
 
   def trim_line: Bytes =
     if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
       subSequence(0, length - 2)
     else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
       subSequence(0, length - 1)
     else this
 
 
   /* streams */
 
   def stream(): ByteArrayInputStream = new ByteArrayInputStream(bytes, offset, length)
 
   def write_stream(stream: OutputStream): Unit = stream.write(bytes, offset, length)
 
 
   /* XZ data compression */
 
   def uncompress(cache: XZ.Cache = XZ.Cache()): Bytes =
     using(new XZInputStream(stream(), cache))(Bytes.read_stream(_, hint = length))
 
   def compress(options: XZ.Options = XZ.options(), cache: XZ.Cache = XZ.Cache()): Bytes = {
     val result = new ByteArrayOutputStream(length)
     using(new XZOutputStream(result, options, cache))(write_stream(_))
     new Bytes(result.toByteArray, 0, result.size)
   }
 
   def maybe_compress(
     options: XZ.Options = XZ.options(),
     cache: XZ.Cache = XZ.Cache()
   ) : (Boolean, Bytes) = {
     val compressed = compress(options = options, cache = cache)
     if (compressed.length < length) (true, compressed) else (false, this)
   }
 }
diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML
+++ b/src/Pure/System/isabelle_system.ML
@@ -1,186 +1,194 @@
 (*  Title:      Pure/System/isabelle_system.ML
     Author:     Makarius
 
 Isabelle system support.
 *)
 
 signature ISABELLE_SYSTEM =
 sig
   val bash_process: Bash.params -> Process_Result.T
   val bash_output: string -> string * int
   val bash: string -> int
   val bash_functions: unit -> string list
   val check_bash_function: Proof.context -> string * Position.T -> string
   val absolute_path: Path.T -> string
   val make_directory: Path.T -> Path.T
   val copy_dir: Path.T -> Path.T -> unit
   val copy_file: Path.T -> Path.T -> unit
   val copy_file_base: Path.T * Path.T -> Path.T -> unit
   val create_tmp_path: string -> string -> Path.T
   val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a
   val rm_tree: Path.T -> unit
   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
   val isabelle_name: unit -> string
   val identification: unit -> string
 end;
 
 structure Isabelle_System: ISABELLE_SYSTEM =
 struct
 
 (* bash *)
 
 val absolute_path = Path.implode o File.absolute_path;
 
 fun bash_process params =
   let
     val {script, input, cwd, putenv, redirect, timeout, description} =
       Bash.dest_params params;
     val run =
       [Bash.server_run, script, input,
         let open XML.Encode in YXML.string_of_body (option (string o absolute_path) cwd) end,
         let open XML.Encode in YXML.string_of_body o list (pair string string) end
           (("ISABELLE_TMP", getenv "ISABELLE_TMP") :: putenv),
         Value.print_bool redirect,
         Value.print_real (Time.toReal timeout),
         description];
 
     val address = Options.default_string \<^system_option>\<open>bash_process_address\<close>;
     val password = Options.default_string \<^system_option>\<open>bash_process_password\<close>;
 
     val _ = address = "" andalso raise Fail "Bad bash_process server address";
     fun with_streams f = Socket_IO.with_streams' f address password;
 
     fun kill (SOME uuid) =
           with_streams (fn s => Byte_Message.write_message_string (#2 s) [Bash.server_kill, uuid])
       | kill NONE = ();
   in
     Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
       let
         fun err () = raise Fail "Malformed result from bash_process server";
         fun loop maybe_uuid s =
           (case restore_attributes Byte_Message.read_message_string (#1 s) of
             SOME (head :: args) =>
               if head = Bash.server_uuid andalso length args = 1 then
                 loop (SOME (hd args)) s
               else if head = Bash.server_interrupt andalso null args then
                 raise Exn.Interrupt
               else if head = Bash.server_failure andalso length args = 1 then
                 raise Fail (hd args)
               else if head = Bash.server_result andalso length args >= 4 then
                 let
                   val a :: b :: c :: d :: lines = args;
                   val rc = Value.parse_int a;
                   val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c);
                   val (out_lines, err_lines) = chop (Value.parse_int d) lines;
                 in
                   if rc = Process_Result.timeout_rc then raise Timeout.TIMEOUT elapsed
                   else
                     Process_Result.make
                      {rc = rc,
                       out_lines = out_lines,
                       err_lines = err_lines,
                       timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}}
                  end
                else err ()
           | _ => err ())
           handle exn => (kill maybe_uuid; Exn.reraise exn);
       in with_streams (fn s => (Byte_Message.write_message_string (#2 s) run; loop NONE s)) end) ()
   end;
 
 val bash = Bash.script #> bash_process #> Process_Result.print #> Process_Result.rc;
 
 fun bash_output s =
   let
     val res = bash_process (Bash.script s);
     val _ = warning (Process_Result.err res);
   in (Process_Result.out res, Process_Result.rc res) end;
 
 
 (* bash functions *)
 
 fun bash_functions () =
   bash_process (Bash.script "declare -Fx")
   |> Process_Result.check
   |> Process_Result.out_lines
   |> map_filter (space_explode " " #> try List.last);
 
 fun check_bash_function ctxt arg =
   Completion.check_entity Markup.bash_functionN
     (bash_functions () |> map (rpair Position.none)) ctxt arg;
 
 
 (* directory and file operations *)
 
 fun scala_function name = ignore o Scala.function name o map absolute_path;
 
 fun make_directory path = (scala_function "make_directory" [path]; path);
 
 fun copy_dir src dst = scala_function "copy_dir" [src, dst];
 
 fun copy_file src dst = scala_function "copy_file" [src, dst];
 
 fun copy_file_base (base_dir, src) target_dir =
   ignore (Scala.function "copy_file_base"
     [absolute_path base_dir, Path.implode src, absolute_path target_dir]);
 
 
 (* tmp files *)
 
 fun create_tmp_path name ext =
   let
     val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext);
     val _ = File.exists path andalso
       raise Fail ("Temporary file already exists: " ^ Path.print path);
   in path end;
 
 fun with_tmp_file name ext f =
   let val path = create_tmp_path name ext
   in Exn.release (Exn.capture f path before ignore (try File.rm path)) end;
 
 
 (* tmp dirs *)
 
 fun rm_tree path = scala_function "rm_tree" [path];
 
 fun with_tmp_dir name f =
   let val path = create_tmp_path name ""
   in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end;
 
 
 (* download file *)
 
 val download = Bytes.string #> Scala.function1_bytes "download";
 
 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" "";
 
 fun isabelle_identifier () = try getenv_strict "ISABELLE_IDENTIFIER";
 
 fun isabelle_heading () =
   (case isabelle_identifier () of
     NONE => ""
   | SOME version => " (" ^ version ^ ")");
 
 fun isabelle_name () = getenv_strict "ISABELLE_NAME";
 
 fun identification () =
   "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading ();
 
 end;
diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,323 +1,325 @@
 /*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
 Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
 import scala.tools.nsc.interpreter.{IMain, Results}
 import scala.tools.nsc.interpreter.shell.ReplReporterImpl
 
 object Scala {
   /** registered functions **/
 
   abstract class Fun(val name: String, val thread: Boolean = false) {
     override def toString: String = name
     def multi: Boolean = true
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def invoke(args: List[Bytes]): List[Bytes]
   }
 
   abstract class Fun_Strings(name: String, thread: Boolean = false)
   extends Fun(name, thread = thread) {
     override def invoke(args: List[Bytes]): List[Bytes] =
       apply(args.map(_.text)).map(Bytes.apply)
     def apply(args: List[String]): List[String]
   }
 
   abstract class Fun_String(name: String, thread: Boolean = false)
   extends Fun_Strings(name, thread = thread) {
     override def multi: Boolean = false
     override def apply(args: List[String]): List[String] =
       List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }
 
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =
     Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
 
 
 
   /** demo functions **/
 
   object Echo extends Fun_String("echo") {
     val here = Scala_Project.here
     def apply(arg: String): String = arg
   }
 
   object Sleep extends Fun_String("sleep") {
     val here = Scala_Project.here
     def apply(seconds: String): String = {
       val t =
         seconds match {
           case Value.Double(s) => Time.seconds(s)
           case _ => error("Malformed argument: " + quote(seconds))
         }
       val t0 = Time.now()
       t.sleep()
       val t1 = Time.now()
       (t1 - t0).toString
     }
   }
 
 
 
   /** compiler **/
 
   def class_path(): List[String] =
     for {
       prop <- List("isabelle.scala.classpath", "java.class.path")
       elems = System.getProperty(prop, "") if elems.nonEmpty
       elem <- space_explode(JFile.pathSeparatorChar, elems) if elem.nonEmpty
     } yield elem
 
   object Compiler {
     def default_print_writer: PrintWriter =
       new NewLinePrintWriter(new ConsoleWriter, true)
 
     def context(
       print_writer: PrintWriter = default_print_writer,
       error: String => Unit = Exn.error,
       jar_dirs: List[JFile] = Nil,
       class_loader: Option[ClassLoader] = None
     ): Context = {
       def find_jars(dir: JFile): List[String] =
         File.find_files(dir, file => file.getName.endsWith(".jar")).
           map(File.absolute_name)
 
       val settings = new GenericRunnerSettings(error)
       settings.classpath.value =
         (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
       new Context(settings, print_writer, class_loader)
     }
 
     class Context private [Compiler](
       val settings: GenericRunnerSettings,
       val print_writer: PrintWriter,
       val class_loader: Option[ClassLoader]
     ) {
       override def toString: String = settings.toString
 
       val interp: IMain =
         new IMain(settings, new ReplReporterImpl(settings, print_writer)) {
           override def parentClassLoader: ClassLoader =
             class_loader getOrElse super.parentClassLoader
         }
     }
 
     def toplevel(interpret: Boolean, source: String): List[String] = {
       val out = new StringWriter
       val interp = Compiler.context(print_writer = new PrintWriter(out)).interp
       val marker = '\u000b'
       val ok =
         interp.withLabel(marker.toString) {
           if (interpret) interp.interpret(source) == Results.Success
           else (new interp.ReadEvalPrint).compile(source)
         }
       out.close()
 
       val Error = """(?s)^\S* error: (.*)$""".r
       val errors =
         space_explode(marker, Library.strip_ansi_color(out.toString)).
           collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
       if (!ok && errors.isEmpty) List("Error") else errors
     }
   }
 
   object Toplevel extends Fun_String("scala_toplevel") {
     val here = Scala_Project.here
     def apply(arg: String): String = {
       val (interpret, source) =
         YXML.parse_body(arg) match {
           case Nil => (false, "")
           case List(XML.Text(source)) => (false, source)
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
         try { Compiler.toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
   }
 
 
 
   /** interpreter thread **/
 
   object Interpreter {
     /* requests */
 
     sealed abstract class Request
     case class Execute(command: Compiler.Context => Unit) extends Request
     case object Shutdown extends Request
 
 
     /* known interpreters */
 
     private val known = Synchronized(Set.empty[Interpreter])
 
     def add(interpreter: Interpreter): Unit = known.change(_ + interpreter)
     def del(interpreter: Interpreter): Unit = known.change(_ - interpreter)
 
     def get[A](which: PartialFunction[Interpreter, A]): Option[A] =
       known.value.collectFirst(which)
   }
 
   class Interpreter(context: Compiler.Context) {
     interpreter =>
 
     private val running = Synchronized[Option[Thread]](None)
     def running_thread(thread: Thread): Boolean = running.value.contains(thread)
     def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
 
     private lazy val thread: Consumer_Thread[Interpreter.Request] =
       Consumer_Thread.fork("Scala.Interpreter") {
         case Interpreter.Execute(command) =>
           try {
             running.change(_ => Some(Thread.currentThread()))
             command(context)
           }
           finally {
             running.change(_ => None)
             Exn.Interrupt.dispose()
           }
           true
         case Interpreter.Shutdown =>
           Interpreter.del(interpreter)
           false
       }
 
     def shutdown(): Unit = {
       thread.send(Interpreter.Shutdown)
       interrupt_thread()
       thread.shutdown()
     }
 
     def execute(command: Compiler.Context => Unit): Unit =
       thread.send(Interpreter.Execute(command))
 
     Interpreter.add(interpreter)
     thread
   }
 
 
 
   /** invoke Scala functions from ML **/
 
   /* invoke function */
 
   object Tag extends Enumeration {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
   def function_thread(name: String): Boolean =
     functions.find(fun => fun.name == name) match {
       case Some(fun) => fun.thread
       case None => false
     }
 
   def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun.invoke(args) } match {
           case Exn.Res(null) => (Tag.NULL, Nil)
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
           case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
         }
       case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
     }
 
 
   /* protocol handler */
 
   class Handler extends Session.Protocol_Handler {
     private var session: Session = null
     private var futures = Map.empty[String, Future[Unit]]
 
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
     override def exit(): Unit = synchronized {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }
 
     private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
       synchronized {
         if (futures.isDefinedAt(id)) {
           session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
           futures -= id
         }
       }
 
     private def cancel(id: String, future: Future[Unit]): Unit = {
       future.cancel()
       result(id, Scala.Tag.INTERRUPT, Nil)
     }
 
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
           def body(): Unit = {
             val (tag, res) = Scala.function_body(name, msg.chunks)
             result(id, tag, res)
           }
           val future =
             if (Scala.function_thread(name)) {
               Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body())
             }
             else Future.fork(body())
           futures += (id -> future)
           true
         case _ => false
       }
     }
 
     private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Cancel_Scala(id) =>
           futures.get(id) match {
             case Some(future) => cancel(id, future)
             case None =>
           }
           true
         case _ => false
       }
     }
 
     override val functions: Session.Protocol_Functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
   }
 }
 
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
   Bytes.Decode_Base64,
   Bytes.Encode_Base64,
+  Bytes.Compress,
+  Bytes.Uncompress,
   Doc.Doc_Names,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
   Isabelle_System.Isabelle_Id,
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems,
   isabelle.atp.SystemOnTPTP.Run_System)