# HG changeset patch
# User wenzelm
# Date 1630231495 -7200
# Node ID a1ccecae6a57397c3a38c009a17deb6fd2d988ed
# Parent  2ee03f7abd8d206eefaea54b120b3758d674e8c4
clarified process description;

diff -r 2ee03f7abd8d -r a1ccecae6a57 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Sat Aug 28 23:11:20 2021 +0200
+++ b/src/Pure/System/bash.scala	Sun Aug 29 12:04:55 2021 +0200
@@ -46,22 +46,29 @@
 
   /* 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
@@ -303,7 +310,7 @@
             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 + ")")
@@ -311,6 +318,7 @@
 
           Exn.capture {
             Bash.process(script,
+              description = description,
               cwd =
                 XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match {
                   case None => null
diff -r 2ee03f7abd8d -r a1ccecae6a57 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Sat Aug 28 23:11:20 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Sun Aug 29 12:04:55 2021 +0200
@@ -40,7 +40,7 @@
 
 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,
diff -r 2ee03f7abd8d -r a1ccecae6a57 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Aug 28 23:11:20 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Sun Aug 29 12:04:55 2021 +0200
@@ -387,6 +387,7 @@
   /* GNU bash */
 
   def bash(script: String,
+    description: String = "",
     cwd: JFile = null,
     env: JMap[String, String] = settings(),
     redirect: Boolean = false,
@@ -397,7 +398,8 @@
     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)
   }