diff --git a/src/Pure/System/bash.scala b/src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala
+++ b/src/Pure/System/bash.scala
@@ -1,386 +1,394 @@
 /*  Title:      Pure/System/bash.scala
     Author:     Makarius
 
 Support for GNU bash: portable external processes with propagation of
 interrupts.
 */
 
 package isabelle
 
 
 import java.util.{LinkedList, List => JList, Map => JMap}
 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile}
 import scala.annotation.tailrec
 import scala.jdk.OptionConverters._
 
 
 object Bash
 {
   /* concrete syntax */
 
   private def bash_chr(c: Byte): String =
   {
     val ch = c.toChar
     ch match {
       case '\t' => "$'\\t'"
       case '\n' => "$'\\n'"
       case '\f' => "$'\\f'"
       case '\r' => "$'\\r'"
       case _ =>
         if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
           Symbol.ascii(ch)
         else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
         else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
         else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
         else  "\\" + ch
     }
   }
 
   def string(s: String): String =
     if (s == "") "\"\""
     else UTF8.bytes(s).iterator.map(bash_chr).mkString
 
   def strings(ss: List[String]): String =
     ss.iterator.map(Bash.string).mkString(" ")
 
 
   /* process and result */
 
+  private def make_description(description: String): String =
+    proper_string(description) getOrElse "bash_process"
+
   type Watchdog = (Time, Process => Boolean)
 
   def process(script: String,
+      description: String = "",
       cwd: JFile = null,
       env: JMap[String, String] = Isabelle_System.settings(),
       redirect: Boolean = false,
       cleanup: () => Unit = () => ()): Process =
-    new Process(script, cwd, env, redirect, cleanup)
+    new Process(script, description, cwd, env, redirect, cleanup)
 
   class Process private[Bash](
       script: String,
+      description: String,
       cwd: JFile,
       env: JMap[String, String],
       redirect: Boolean,
       cleanup: () => Unit)
   {
+    override def toString: String = make_description(description)
+
     private val timing_file = Isabelle_System.tmp_file("bash_timing")
     private val timing = Synchronized[Option[Timing]](None)
     def get_timing: Timing = timing.value getOrElse Timing.zero
 
     private val winpid_file: Option[JFile] =
       if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None
     private val winpid_script =
       winpid_file match {
         case None => script
         case Some(file) =>
           "read < /proc/self/winpid > /dev/null 2> /dev/null\n" +
           """echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script
       }
 
     private val script_file: JFile = Isabelle_System.tmp_file("bash_script")
     File.write(script_file, winpid_script)
 
     private val proc =
       isabelle.setup.Environment.process_builder(
         JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")),
           File.standard_path(timing_file), "bash", File.standard_path(script_file)),
         cwd, env, redirect).start()
 
 
     // channels
 
     val stdin: BufferedWriter =
       new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
 
     val stdout: BufferedReader =
       new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
 
     val stderr: BufferedReader =
       new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
 
 
     // signals
 
     private val group_pid = stdout.readLine
 
     private def process_alive(pid: String): Boolean =
       (for {
         p <- Value.Long.unapply(pid)
         handle <- ProcessHandle.of(p).toScala
       } yield handle.isAlive) getOrElse false
 
     private def root_process_alive(): Boolean =
       winpid_file match {
         case None => process_alive(group_pid)
         case Some(file) =>
           file.exists() && process_alive(Library.trim_line(File.read(file)))
       }
 
     @tailrec private def signal(s: String, count: Int = 1): Boolean =
     {
       count <= 0 ||
       {
         isabelle.setup.Environment.kill_process(group_pid, s)
         val running =
           root_process_alive() ||
           isabelle.setup.Environment.kill_process(group_pid, "0")
         if (running) {
           Time.seconds(0.1).sleep()
           signal(s, count - 1)
         }
         else false
       }
     }
 
     def terminate(): Unit = Isabelle_Thread.try_uninterruptible
     {
       signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL")
       proc.destroy()
       do_cleanup()
     }
 
     def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
     {
       isabelle.setup.Environment.kill_process(group_pid, "INT")
     }
 
 
     // JVM shutdown hook
 
     private val shutdown_hook = Isabelle_Thread.create(() => terminate())
 
     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
     catch { case _: IllegalStateException => }
 
 
     // cleanup
 
     private def do_cleanup(): Unit =
     {
       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
       catch { case _: IllegalStateException => }
 
       script_file.delete()
       winpid_file.foreach(_.delete())
 
       timing.change {
         case None =>
           if (timing_file.isFile) {
             val t =
               Word.explode(File.read(timing_file)) match {
                 case List(Value.Long(elapsed), Value.Long(cpu)) =>
                   Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
                 case _ => Timing.zero
               }
             timing_file.delete
             Some(t)
           }
           else Some(Timing.zero)
         case some => some
       }
 
       cleanup()
     }
 
 
     // join
 
     def join(): Int =
     {
       val rc = proc.waitFor()
       do_cleanup()
       rc
     }
 
 
     // result
 
     def result(
       input: String = "",
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
       watchdog: Option[Watchdog] = None,
       strict: Boolean = true): Process_Result =
     {
       val in =
         if (input.isEmpty) Future.value(stdin.close())
         else Future.thread("bash_stdin") { stdin.write(input); stdin.flush(); stdin.close(); }
       val out_lines =
         Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
       val err_lines =
         Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
 
       val watchdog_thread =
         for ((time, check) <- watchdog)
         yield {
           Future.thread("bash_watchdog") {
             while (proc.isAlive) {
               time.sleep()
               if (check(this)) interrupt()
             }
           }
         }
 
       val rc =
         try { join() }
         catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc }
 
       watchdog_thread.foreach(_.cancel())
 
       in.join
       out_lines.join
       err_lines.join
 
       if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt()
 
       Process_Result(rc, out_lines.join, err_lines.join, get_timing)
     }
   }
 
 
   /* server */
 
   object Server
   {
     // input messages
     private val RUN = "run"
     private val KILL = "kill"
 
     // output messages
     private val UUID = "uuid"
     private val INTERRUPT = "interrupt"
     private val FAILURE = "failure"
     private val RESULT = "result"
 
     def start(port: Int = 0, debugging: => Boolean = false): Server =
     {
       val server = new Server(port, debugging)
       server.start()
       server
     }
   }
 
   class Server private(port: Int, debugging: => Boolean)
     extends isabelle.Server.Handler(port)
   {
     server =>
 
     private val _processes = Synchronized(Map.empty[UUID.T, Bash.Process])
 
     override def stop(): Unit =
     {
       for ((_, process) <- _processes.value) process.terminate()
       super.stop()
     }
 
     override def handle(connection: isabelle.Server.Connection): Unit =
     {
       def reply(chunks: List[String]): Unit =
         connection.write_byte_message(chunks.map(Bytes.apply))
 
       def reply_failure(exn: Throwable): Unit =
         reply(
           if (Exn.is_interrupt(exn)) List(Server.INTERRUPT)
           else List(Server.FAILURE, Exn.message(exn)))
 
       def reply_result(result: Process_Result): Unit =
         reply(
           Server.RESULT ::
           result.rc.toString ::
           result.timing.elapsed.ms.toString ::
           result.timing.cpu.ms.toString ::
           result.out_lines.length.toString ::
           result.out_lines :::
           result.err_lines)
 
       connection.read_byte_message().map(_.map(_.text)) match {
         case None =>
 
         case Some(List(Server.KILL, UUID(uuid))) =>
           if (debugging) Output.writeln("kill " + uuid)
           _processes.value.get(uuid).foreach(_.terminate())
 
         case Some(List(Server.RUN, script, input, cwd, putenv,
             Value.Boolean(redirect), Value.Seconds(timeout), description)) =>
           val uuid = UUID.random()
 
-          val descr = proper_string(description) getOrElse "bash_process"
+          val descr = make_description(description)
           if (debugging) {
             Output.writeln(
               "start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")")
           }
 
           Exn.capture {
             Bash.process(script,
+              description = description,
               cwd =
                 XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match {
                   case None => null
                   case Some(s) => Path.explode(s).file
                 },
               env =
                 Isabelle_System.settings(
                   XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))(
                     YXML.parse_body(putenv))),
               redirect= redirect)
           }
           match {
             case Exn.Exn(exn) => reply_failure(exn)
             case Exn.Res(process) =>
               _processes.change(processes => processes + (uuid -> process))
               reply(List(Server.UUID, uuid.toString))
 
               Isabelle_Thread.fork(name = "bash_process") {
                 @volatile var is_timeout = false
                 val watchdog: Option[Watchdog] =
                   if (timeout.is_zero) None else Some((timeout, _ => { is_timeout = true; true }))
 
                 Exn.capture { process.result(input = input, watchdog = watchdog, strict = false) }
                 match {
                   case Exn.Exn(exn) => reply_failure(exn)
                   case Exn.Res(res0) =>
                     val res = if (!res0.ok && is_timeout) res0.timeout_rc else res0
                     if (debugging) {
                       Output.writeln(
                         "stop " + quote(descr) + " (uuid=" + uuid + ", return_code=" + res.rc + ")")
                     }
                     reply_result(res)
                 }
 
                 _processes.change(provers => provers - uuid)
               }
 
               connection.await_close()
           }
 
         case Some(_) => reply_failure(ERROR("Bad protocol message"))
       }
     }
   }
 
   class Handler extends Session.Protocol_Handler
   {
     private var server: Server = null
 
     override def init(session: Session): Unit =
     {
       exit()
       server = Server.start(debugging = session.session_options.bool("bash_process_debugging"))
     }
 
     override def exit(): Unit =
     {
       if (server != null) {
         server.stop()
         server = null
       }
     }
 
     override def prover_options(options: Options): Options =
     {
       val address = if (server == null) "" else server.address
       val password = if (server == null) "" else server.password
       options +
         ("bash_process_address=" + address) +
         ("bash_process_password=" + password)
     }
   }
 }
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,185 +1,185 @@
 (*  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 -> string
   val download_file: string -> Path.T -> unit
   val decode_base64: string -> string
   val encode_base64: string -> string
   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: string} =
+    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 (#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 (#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 (#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 = Scala.function1 "download";
 
 fun download_file url path = File.write path (download url);
 
 
 (* base64 *)
 
 val decode_base64 = Scala.function1 "decode_base64";
 val encode_base64 = Scala.function1 "encode_base64";
 
 
 (* 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/" ^ isabelle_id () ^ isabelle_heading ();
 
 end;
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,506 +1,508 @@
 /*  Title:      Pure/System/isabelle_system.scala
     Author:     Makarius
 
 Miscellaneous Isabelle system operations.
 */
 
 package isabelle
 
 
 import java.util.{Map => JMap, HashMap}
 import java.io.{File => JFile, IOException}
 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
   StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 
 import scala.jdk.CollectionConverters._
 
 
 object Isabelle_System
 {
   /* settings */
 
   def settings(putenv: List[(String, String)] = Nil): JMap[String, String] =
   {
     val env0 = isabelle.setup.Environment.settings()
     if (putenv.isEmpty) env0
     else {
       val env = new HashMap(env0)
       for ((a, b) <- putenv) env.put(a, b)
       env
     }
   }
 
   def getenv(name: String, env: JMap[String, String] = settings()): String =
     Option(env.get(name)).getOrElse("")
 
   def getenv_strict(name: String, env: JMap[String, String] = settings()): String =
     proper_string(getenv(name, env)) getOrElse
       error("Undefined Isabelle environment variable: " + quote(name))
 
 
   /* services */
 
   abstract class Service
 
   @volatile private var _services: Option[List[Class[Service]]] = None
 
   def services(): List[Class[Service]] =
   {
     if (_services.isEmpty) init()  // unsynchronized check
     _services.get
   }
 
   def make_services[C](c: Class[C]): List[C] =
     for { c1 <- services() if Library.is_subclass(c1, c) }
       yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
 
 
   /* init settings + services */
 
   def make_services(): List[Class[Service]] =
   {
     def make(where: String, names: List[String]): List[Class[Service]] =
     {
       for (name <- names) yield {
         def err(msg: String): Nothing =
           error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
         try { Class.forName(name).asInstanceOf[Class[Service]] }
         catch {
           case _: ClassNotFoundException => err("Class not found")
           case exn: Throwable => err(Exn.message(exn))
         }
       }
     }
 
     def from_env(variable: String): List[Class[Service]] =
       make(quote(variable), space_explode(':', getenv_strict(variable)))
 
     def from_jar(platform_jar: String): List[Class[Service]] =
       make(quote(platform_jar),
         isabelle.setup.Build.get_services(JPath.of(platform_jar)).asScala.toList)
 
     from_env("ISABELLE_SCALA_SERVICES") ::: Scala.class_path().flatMap(from_jar)
   }
 
   def init(isabelle_root: String = "", cygwin_root: String = ""): Unit =
   {
     isabelle.setup.Environment.init(isabelle_root, cygwin_root)
     synchronized { if (_services.isEmpty) { _services = Some(make_services()) } }
   }
 
 
   /* getetc -- static distribution parameters */
 
   def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
   {
     val path = root + Path.basic("etc") + Path.basic(name)
     if (path.is_file) {
       Library.trim_split_lines(File.read(path)) match {
         case Nil => None
         case List(s) => Some(s)
         case _ => error("Single line expected in " + path.absolute)
       }
     }
     else None
   }
 
 
   /* Isabelle distribution identification */
 
   def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
       if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
       else error("Failed to identify Isabelle distribution " + root)
     }
 
   object Isabelle_Id extends Scala.Fun_String("isabelle_id")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = isabelle_id()
   }
 
   def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
     getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
       if (Mercurial.is_repository(root)) {
         val hg = Mercurial.repository(root)
         hg.tags(rev = hg.parent())
       }
       else ""
     }
 
   def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
 
   def isabelle_heading(): String =
     isabelle_identifier() match {
       case None => ""
       case Some(version) => " (" + version + ")"
     }
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
   def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
 
 
   /** file-system operations **/
 
   /* scala functions */
 
   private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
     { fun(args.map(Path.explode)); Nil }
 
   private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
     apply_paths(args, { case List(path) => fun(path) })
 
   private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
     apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
 
   private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
     apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
 
   def chmod(arg: String, path: Path): Unit =
     bash("chmod " + arg + " " + File.bash_path(path)).check
 
   def chown(arg: String, path: Path): Unit =
     bash("chown " + arg + " " + File.bash_path(path)).check
 
 
   /* directories */
 
   def make_directory(path: Path): Path =
   {
     if (!path.is_dir) {
       try { Files.createDirectories(path.java_path) }
       catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
     }
     path
   }
 
   def new_directory(path: Path): Path =
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
   def copy_dir(dir1: Path, dir2: Path): Unit =
   {
     val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
     if (!res.ok) {
       cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
     }
   }
 
 
   object Make_Directory extends Scala.Fun_Strings("make_directory")
   {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
   }
 
   object Copy_Dir extends Scala.Fun_Strings("copy_dir")
   {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
   }
 
 
   /* copy files */
 
   def copy_file(src: JFile, dst: JFile): Unit =
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target)) {
       try {
         Files.copy(src.toPath, target.toPath,
           StandardCopyOption.COPY_ATTRIBUTES,
           StandardCopyOption.REPLACE_EXISTING)
       }
       catch {
         case ERROR(msg) =>
           cat_error("Failed to copy file " +
             File.path(src).absolute + " to " + File.path(dst).absolute, msg)
       }
     }
   }
 
   def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
 
   def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit =
   {
     val src1 = src.expand
     val src1_dir = src1.dir
     if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
     copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
   }
 
 
   object Copy_File extends Scala.Fun_Strings("copy_file")
   {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
   }
 
   object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
   {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
   }
 
 
   /* move files */
 
   def move_file(src: JFile, dst: JFile): Unit =
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!File.eq(src, target))
       Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
   }
 
   def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
 
 
   /* symbolic link */
 
   def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit =
   {
     val src_file = src.file
     val dst_file = dst.file
     val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
 
     if (force) target.delete
 
     def cygwin_link(): Unit =
     {
       if (native) {
         error("Failed to create native symlink on Windows: " + quote(src_file.toString) +
           "\n(but it could work as Administrator)")
       }
       else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
     }
 
 
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
       case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
       case _: FileSystemException if Platform.is_windows => cygwin_link()
     }
   }
 
 
   /* tmp files */
 
   def isabelle_tmp_prefix(): JFile =
   {
     val path = Path.explode("$ISABELLE_TMP_PREFIX")
     path.file.mkdirs  // low-level mkdirs to avoid recursion via Isabelle environment
     File.platform_file(path)
   }
 
   def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
   {
     val suffix = if (ext == "") "" else "." + ext
     val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
     file.deleteOnExit
     file
   }
 
   def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
   {
     val file = tmp_file(name, ext)
     try { body(File.path(file)) } finally { file.delete }
   }
 
 
   /* tmp dirs */
 
   def rm_tree(root: JFile): Unit =
   {
     root.delete
     if (root.isDirectory) {
       Files.walkFileTree(root.toPath,
         new SimpleFileVisitor[JPath] {
           override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
             try { Files.deleteIfExists(file) }
             catch { case _: IOException => }
             FileVisitResult.CONTINUE
           }
 
           override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
           {
             if (e == null) {
               try { Files.deleteIfExists(dir) }
               catch { case _: IOException => }
               FileVisitResult.CONTINUE
             }
             else throw e
           }
         }
       )
     }
   }
 
   def rm_tree(root: Path): Unit = rm_tree(root.file)
 
   object Rm_Tree extends Scala.Fun_Strings("rm_tree")
   {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
   }
 
   def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
   {
     val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
     dir.deleteOnExit
     dir
   }
 
   def with_tmp_dir[A](name: String)(body: Path => A): A =
   {
     val dir = tmp_dir(name)
     try { body(File.path(dir)) } finally { rm_tree(dir) }
   }
 
 
   /* quasi-atomic update of directory */
 
   def update_directory(dir: Path, f: Path => Unit): Unit =
   {
     val new_dir = dir.ext("new")
     val old_dir = dir.ext("old")
 
     rm_tree(new_dir)
     rm_tree(old_dir)
 
     f(new_dir)
 
     if (dir.is_dir) move_file(dir, old_dir)
     move_file(new_dir, dir)
     rm_tree(old_dir)
   }
 
 
 
   /** external processes **/
 
   /* GNU bash */
 
   def bash(script: String,
+    description: String = "",
     cwd: JFile = null,
     env: JMap[String, String] = settings(),
     redirect: Boolean = false,
     input: String = "",
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
     watchdog: Option[Bash.Watchdog] = None,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()): Process_Result =
   {
-    Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
+    Bash.process(script,
+      description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
       result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr,
         watchdog = watchdog, strict = strict)
   }
 
   private lazy val gnutar_check: Boolean =
     try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
     catch { case ERROR(_) => false }
 
   def gnutar(
     args: String,
     dir: Path = Path.current,
     original_owner: Boolean = false,
     strip: Int = 0,
     redirect: Boolean = false): Process_Result =
   {
     val options =
       (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
       (if (original_owner) "" else "--owner=root --group=staff ") +
       (if (strip <= 0) "" else "--strip-components=" + strip + " ")
 
     if (gnutar_check) bash("tar " + options + args, redirect = redirect)
     else error("Expected to find GNU tar executable")
   }
 
   def require_command(cmd: String, test: String = "--version"): Unit =
   {
     if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd))
   }
 
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =
     bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
 
   def pdf_viewer(arg: Path): Unit =
     bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
 
   def open_external_file(name: String): Boolean =
   {
     val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
     val external =
       ext.nonEmpty &&
       Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
     if (external) {
       if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
       else open(name)
     }
     external
   }
 
   def export_isabelle_identifier(isabelle_identifier: String): String =
     if (isabelle_identifier == "") ""
     else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
 
 
   /** Isabelle resources **/
 
   /* repository clone with Admin */
 
   def admin(): Boolean = Path.explode("~~/Admin").is_dir
 
 
   /* default logic */
 
   def default_logic(args: String*): String =
   {
     args.find(_ != "") match {
       case Some(logic) => logic
       case None => getenv_strict("ISABELLE_LOGIC")
     }
   }
 
 
   /* download file */
 
   def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
   {
     val url = Url(url_name)
     progress.echo("Getting " + quote(url_name))
     try { HTTP.Client.get(url) }
     catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
   }
 
   def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
     Bytes.write(file, download(url_name, progress = progress).bytes)
 
   object Download extends Scala.Fun("download", thread = true)
   {
     val here = Scala_Project.here
     override def invoke(args: List[Bytes]): List[Bytes] =
       args match { case List(url) => List(download(url.text).bytes) }
   }
 
 
   /* repositories */
 
   val isabelle_repository: Mercurial.Server =
     Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
 
   val afp_repository: Mercurial.Server =
     Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
 
   def official_releases(): List[String] =
     Library.trim_split_lines(
       isabelle_repository.read_file(Path.explode("Admin/Release/official")))
 }