clarified modules;
authorwenzelm
Tue Oct 18 16:03:30 2016 +0200 (2016-10-18)
changeset 6430496bc94c87a81
parent 64303 605351c7ef97
child 64305 4bdea66b01b8
clarified modules;
src/HOL/Library/Old_SMT/old_smt_solver.ML
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/SMT/smt_solver.ML
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_release.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/other_isabelle.scala
src/Pure/Admin/remote_dmg.scala
src/Pure/General/file.ML
src/Pure/General/file.scala
src/Pure/General/mercurial.scala
src/Pure/General/ssh.scala
src/Pure/ROOT.ML
src/Pure/System/bash.ML
src/Pure/System/bash.scala
src/Pure/System/bash_syntax.ML
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Tue Oct 18 15:31:08 2016 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Tue Oct 18 16:03:30 2016 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  fun make_cmd command options problem_path proof_path =
     1.6    space_implode " "
     1.7 -    ("(exec 2>&1;" :: map File.bash_string (command () @ options) @
     1.8 +    ("(exec 2>&1;" :: map Bash.string (command () @ options) @
     1.9        [File.bash_path problem_path, ")", ">", File.bash_path proof_path])
    1.10  
    1.11  fun trace_and ctxt msg f x =
     2.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 18 15:31:08 2016 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Tue Oct 18 16:03:30 2016 +0200
     2.3 @@ -1028,7 +1028,7 @@
     2.4            val outcome =
     2.5              let
     2.6                val code =
     2.7 -                Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
     2.8 +                Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
     2.9                        \\"$KODKODI/bin/kodkodi\"" ^
    2.10                        (if ms >= 0 then " -max-msecs " ^ string_of_int ms
    2.11                         else "") ^
     3.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 18 15:31:08 2016 +0200
     3.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Tue Oct 18 16:03:30 2016 +0200
     3.3 @@ -49,7 +49,7 @@
     3.4  local
     3.5  
     3.6  fun make_command command options problem_path proof_path =
     3.7 -  "(exec 2>&1;" :: map File.bash_string (command () @ options) @
     3.8 +  "(exec 2>&1;" :: map Bash.string (command () @ options) @
     3.9    [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
    3.10    |> space_implode " "
    3.11  
     4.1 --- a/src/Pure/Admin/build_history.scala	Tue Oct 18 15:31:08 2016 +0200
     4.2 +++ b/src/Pure/Admin/build_history.scala	Tue Oct 18 16:03:30 2016 +0200
     4.3 @@ -190,7 +190,7 @@
     4.4        val build_start = Date.now()
     4.5        val build_args1 = List("-v", "-j" + processes) ::: build_args
     4.6        val build_result =
     4.7 -        other_isabelle("build " + File.bash_args(build_args1), redirect = true, echo = verbose)
     4.8 +        other_isabelle("build " + Bash.strings(build_args1), redirect = true, echo = verbose)
     4.9        val build_end = Date.now()
    4.10  
    4.11        val log_path =
    4.12 @@ -373,7 +373,7 @@
    4.13      options: String = "",
    4.14      args: String = ""): List[(String, Bytes)] =
    4.15    {
    4.16 -    val isabelle_admin = ssh.remote_path(isabelle_repos_self + Path.explode("Admin"))
    4.17 +    val isabelle_admin = ssh.bash_path(isabelle_repos_self + Path.explode("Admin"))
    4.18  
    4.19  
    4.20      /* prepare repository clones */
    4.21 @@ -384,19 +384,19 @@
    4.22      if (self_update) {
    4.23        isabelle_hg.pull()
    4.24        isabelle_hg.update(clean = true)
    4.25 -      ssh.execute(File.bash_string(isabelle_admin + "/build") + " jars_fresh").check
    4.26 +      ssh.execute(Bash.string(isabelle_admin + "/build") + " jars_fresh").check
    4.27      }
    4.28  
    4.29      Mercurial.setup_repository(
    4.30 -      ssh.remote_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
    4.31 +      ssh.bash_path(isabelle_repos_self), isabelle_repos_other, ssh = Some(ssh))
    4.32  
    4.33  
    4.34      /* Admin/build_history */
    4.35  
    4.36      val result =
    4.37        ssh.execute(
    4.38 -        File.bash_string(isabelle_admin + "/build_history") + " " + options + " " +
    4.39 -          File.bash_string(ssh.remote_path(isabelle_repos_other)) + " " + args,
    4.40 +        Bash.string(isabelle_admin + "/build_history") + " " + options + " " +
    4.41 +          ssh.bash_path(isabelle_repos_other) + " " + args,
    4.42          progress_stderr = progress.echo(_)).check
    4.43  
    4.44      for (line <- result.out_lines; log = Path.explode(line))
     5.1 --- a/src/Pure/Admin/build_release.scala	Tue Oct 18 15:31:08 2016 +0200
     5.2 +++ b/src/Pure/Admin/build_release.scala	Tue Oct 18 16:03:30 2016 +0200
     5.3 @@ -76,8 +76,8 @@
     5.4          progress.bash(
     5.5            "isabelle makedist -d " + File.bash_path(base_dir) + jobs_option +
     5.6              (if (official_release) " -O" else "") +
     5.7 -            (if (release_name != "") " -r " + File.bash_string(release_name) else "") +
     5.8 -            (if (rev != "") " " + File.bash_string(rev) else ""),
     5.9 +            (if (release_name != "") " -r " + Bash.string(release_name) else "") +
    5.10 +            (if (rev != "") " " + Bash.string(rev) else ""),
    5.11            echo = true).check
    5.12        }
    5.13        Library.trim_line(File.read(isabelle_ident_file))
    5.14 @@ -98,8 +98,8 @@
    5.15          progress.echo("\nApplication bundle for " + platform_family + ": " + bundle_archive.implode)
    5.16          progress.bash(
    5.17            "isabelle makedist_bundle " + File.bash_path(release_info.dist_archive) +
    5.18 -            " " + File.bash_string(platform_family) +
    5.19 -            (if (remote_mac == "") "" else " " + File.bash_string(remote_mac)),
    5.20 +            " " + Bash.string(platform_family) +
    5.21 +            (if (remote_mac == "") "" else " " + Bash.string(remote_mac)),
    5.22            echo = true).check
    5.23        }
    5.24      }
     6.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 15:31:08 2016 +0200
     6.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 16:03:30 2016 +0200
     6.3 @@ -123,8 +123,7 @@
     6.4                    isabelle_repos_source = isabelle_dev_source,
     6.5                    self_update = !r.shared_home,
     6.6                    options =
     6.7 -                    r.options + " -f -r " + File.bash_string(rev) +
     6.8 -                      " -N " + File.bash_string(task_name),
     6.9 +                    r.options + " -f -r " + Bash.string(rev) + " -N " + Bash.string(task_name),
    6.10                    args = r.args)
    6.11                for ((log, bytes) <- results)
    6.12                  Bytes.write(logger.log_dir + Path.explode(log), bytes)
     7.1 --- a/src/Pure/Admin/other_isabelle.scala	Tue Oct 18 15:31:08 2016 +0200
     7.2 +++ b/src/Pure/Admin/other_isabelle.scala	Tue Oct 18 16:03:30 2016 +0200
     7.3 @@ -16,7 +16,7 @@
     7.4  
     7.5    def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     7.6      progress.bash(
     7.7 -      "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script,
     7.8 +      "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + script,
     7.9        env = null, cwd = isabelle_home.file, redirect = redirect)
    7.10  
    7.11    def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result =
     8.1 --- a/src/Pure/Admin/remote_dmg.scala	Tue Oct 18 15:31:08 2016 +0200
     8.2 +++ b/src/Pure/Admin/remote_dmg.scala	Tue Oct 18 16:03:30 2016 +0200
     8.3 @@ -13,13 +13,13 @@
     8.4    {
     8.5      ssh.with_tmp_dir(remote_dir =>
     8.6        {
     8.7 -        val cd = "cd " + File.bash_string(ssh.remote_path(remote_dir)) + "; "
     8.8 +        val cd = "cd " + ssh.bash_path(remote_dir) + "; "
     8.9  
    8.10          ssh.write_file(remote_dir + Path.explode("dmg.tar.gz"), tar_gz_file)
    8.11          ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
    8.12          ssh.execute(
    8.13            cd + "hdiutil create -srcfolder root" +
    8.14 -            (if (volume_name == "") "" else " -volname " + File.bash_string(volume_name)) +
    8.15 +            (if (volume_name == "") "" else " -volname " + Bash.string(volume_name)) +
    8.16              " dmg.dmg").check
    8.17          ssh.read_file(remote_dir + Path.explode("dmg.dmg"), dmg_file)
    8.18        })
     9.1 --- a/src/Pure/General/file.ML	Tue Oct 18 15:31:08 2016 +0200
     9.2 +++ b/src/Pure/General/file.ML	Tue Oct 18 16:03:30 2016 +0200
     9.3 @@ -8,8 +8,6 @@
     9.4  sig
     9.5    val standard_path: Path.T -> string
     9.6    val platform_path: Path.T -> string
     9.7 -  val bash_string: string -> string
     9.8 -  val bash_args: string list -> string
     9.9    val bash_path: Path.T -> string
    9.10    val full_path: Path.T -> Path.T -> Path.T
    9.11    val tmp_path: Path.T -> Path.T
    9.12 @@ -46,26 +44,7 @@
    9.13  val standard_path = Path.implode o Path.expand;
    9.14  val platform_path = ML_System.platform_path o standard_path;
    9.15  
    9.16 -fun bash_string "" = "\"\""
    9.17 -  | bash_string str =
    9.18 -      str |> translate_string (fn ch =>
    9.19 -        let val c = ord ch in
    9.20 -          (case ch of
    9.21 -            "\t" => "$'\\t'"
    9.22 -          | "\n" => "$'\\n'"
    9.23 -          | "\f" => "$'\\f'"
    9.24 -          | "\r" => "$'\\r'"
    9.25 -          | _ =>
    9.26 -              if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
    9.27 -                exists_string (fn c => c = ch) "-./:_" then ch
    9.28 -              else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
    9.29 -              else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
    9.30 -              else "\\" ^ ch)
    9.31 -        end);
    9.32 -
    9.33 -val bash_args = space_implode " " o map bash_string;
    9.34 -
    9.35 -val bash_path = bash_string o standard_path;
    9.36 +val bash_path = Bash_Syntax.string o standard_path;
    9.37  
    9.38  
    9.39  (* full_path *)
    10.1 --- a/src/Pure/General/file.scala	Tue Oct 18 15:31:08 2016 +0200
    10.2 +++ b/src/Pure/General/file.scala	Tue Oct 18 16:03:30 2016 +0200
    10.3 @@ -108,33 +108,8 @@
    10.4  
    10.5    /* bash path */
    10.6  
    10.7 -  private def bash_chr(c: Byte): String =
    10.8 -  {
    10.9 -    val ch = c.toChar
   10.10 -    ch match {
   10.11 -      case '\t' => "$'\\t'"
   10.12 -      case '\n' => "$'\\n'"
   10.13 -      case '\f' => "$'\\f'"
   10.14 -      case '\r' => "$'\\r'"
   10.15 -      case _ =>
   10.16 -        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
   10.17 -          Symbol.ascii(ch)
   10.18 -        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
   10.19 -        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
   10.20 -        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
   10.21 -        else  "\\" + ch
   10.22 -    }
   10.23 -  }
   10.24 -
   10.25 -  def bash_string(s: String): String =
   10.26 -    if (s == "") "\"\""
   10.27 -    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
   10.28 -
   10.29 -  def bash_args(args: List[String]): String =
   10.30 -    args.iterator.map(bash_string(_)).mkString(" ")
   10.31 -
   10.32 -  def bash_path(path: Path): String = bash_string(standard_path(path))
   10.33 -  def bash_path(file: JFile): String = bash_string(standard_path(file))
   10.34 +  def bash_path(path: Path): String = Bash.string(standard_path(path))
   10.35 +  def bash_path(file: JFile): String = Bash.string(standard_path(file))
   10.36  
   10.37  
   10.38    /* directory entries */
    11.1 --- a/src/Pure/General/mercurial.scala	Tue Oct 18 15:31:08 2016 +0200
    11.2 +++ b/src/Pure/General/mercurial.scala	Tue Oct 18 16:03:30 2016 +0200
    11.3 @@ -16,7 +16,7 @@
    11.4    /* command-line syntax */
    11.5  
    11.6    def optional(s: String, prefix: String = ""): String =
    11.7 -    if (s == "") "" else " " + prefix + " " + File.bash_string(s)
    11.8 +    if (s == "") "" else " " + prefix + " " + Bash.string(s)
    11.9  
   11.10    def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
   11.11    def opt_rev(s: String): String = optional(s, "--rev")
   11.12 @@ -40,7 +40,7 @@
   11.13        case None => Isabelle_System.mkdirs(hg.root.dir)
   11.14        case Some(ssh) => ssh.mkdirs(hg.root.dir)
   11.15      }
   11.16 -    hg.command("clone", File.bash_string(source) + " " + File.bash_path(hg.root), options).check
   11.17 +    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
   11.18      hg
   11.19    }
   11.20  
    12.1 --- a/src/Pure/General/ssh.scala	Tue Oct 18 15:31:08 2016 +0200
    12.2 +++ b/src/Pure/General/ssh.scala	Tue Oct 18 16:03:30 2016 +0200
    12.3 @@ -243,6 +243,7 @@
    12.4      }
    12.5      def expand_path(path: Path): Path = path.expand_env(settings)
    12.6      def remote_path(path: Path): String = expand_path(path).implode
    12.7 +    def bash_path(path: Path): String = Bash.string(remote_path(path))
    12.8  
    12.9      def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path))
   12.10      def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2))
   12.11 @@ -324,7 +325,7 @@
   12.12      /* tmp dirs */
   12.13  
   12.14      def rm_tree(remote_dir: String): Unit =
   12.15 -      execute("rm -r -f " + File.bash_string(remote_dir)).check
   12.16 +      execute("rm -r -f " + Bash.string(remote_dir)).check
   12.17  
   12.18      def tmp_dir(): String =
   12.19        execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
    13.1 --- a/src/Pure/ROOT.ML	Tue Oct 18 15:31:08 2016 +0200
    13.2 +++ b/src/Pure/ROOT.ML	Tue Oct 18 16:03:30 2016 +0200
    13.3 @@ -67,6 +67,7 @@
    13.4  ML_file "PIDE/xml.ML";
    13.5  ML_file "General/path.ML";
    13.6  ML_file "General/url.ML";
    13.7 +ML_file "System/bash_syntax.ML";
    13.8  ML_file "General/file.ML";
    13.9  ML_file "General/long_name.ML";
   13.10  ML_file "General/binding.ML";
    14.1 --- a/src/Pure/System/bash.ML	Tue Oct 18 15:31:08 2016 +0200
    14.2 +++ b/src/Pure/System/bash.ML	Tue Oct 18 16:03:30 2016 +0200
    14.3 @@ -6,6 +6,8 @@
    14.4  
    14.5  signature BASH =
    14.6  sig
    14.7 +  val string: string -> string
    14.8 +  val strings: string list -> string
    14.9    val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
   14.10  end;
   14.11  
   14.12 @@ -14,6 +16,9 @@
   14.13  structure Bash: BASH =
   14.14  struct
   14.15  
   14.16 +val string = Bash_Syntax.string;
   14.17 +val strings = Bash_Syntax.strings;
   14.18 +
   14.19  val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   14.20    let
   14.21      datatype result = Wait | Signal | Result of int;
   14.22 @@ -105,6 +110,9 @@
   14.23  structure Bash: BASH =
   14.24  struct
   14.25  
   14.26 +val string = Bash_Syntax.string;
   14.27 +val strings = Bash_Syntax.strings;
   14.28 +
   14.29  val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   14.30    let
   14.31      datatype result = Wait | Signal | Result of int;
    15.1 --- a/src/Pure/System/bash.scala	Tue Oct 18 15:31:08 2016 +0200
    15.2 +++ b/src/Pure/System/bash.scala	Tue Oct 18 16:03:30 2016 +0200
    15.3 @@ -13,6 +13,36 @@
    15.4  
    15.5  object Bash
    15.6  {
    15.7 +  /* concrete syntax */
    15.8 +
    15.9 +  private def bash_chr(c: Byte): String =
   15.10 +  {
   15.11 +    val ch = c.toChar
   15.12 +    ch match {
   15.13 +      case '\t' => "$'\\t'"
   15.14 +      case '\n' => "$'\\n'"
   15.15 +      case '\f' => "$'\\f'"
   15.16 +      case '\r' => "$'\\r'"
   15.17 +      case _ =>
   15.18 +        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch))
   15.19 +          Symbol.ascii(ch)
   15.20 +        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
   15.21 +        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
   15.22 +        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
   15.23 +        else  "\\" + ch
   15.24 +    }
   15.25 +  }
   15.26 +
   15.27 +  def string(s: String): String =
   15.28 +    if (s == "") "\"\""
   15.29 +    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
   15.30 +
   15.31 +  def strings(ss: List[String]): String =
   15.32 +    ss.iterator.map(Bash.string(_)).mkString(" ")
   15.33 +
   15.34 +
   15.35 +  /* process and result */
   15.36 +
   15.37    private class Limited_Progress(proc: Process, progress_limit: Option[Long])
   15.38    {
   15.39      private var count = 0L
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Pure/System/bash_syntax.ML	Tue Oct 18 16:03:30 2016 +0200
    16.3 @@ -0,0 +1,35 @@
    16.4 +(*  Title:      Pure/System/bash_syntax.ML
    16.5 +    Author:     Makarius
    16.6 +
    16.7 +Syntax for GNU bash (see also Pure/System/bash.ML).
    16.8 +*)
    16.9 +
   16.10 +signature BASH_SYNTAX =
   16.11 +sig
   16.12 +  val string: string -> string
   16.13 +  val strings: string list -> string
   16.14 +end;
   16.15 +
   16.16 +structure Bash_Syntax: BASH_SYNTAX =
   16.17 +struct
   16.18 +
   16.19 +fun string "" = "\"\""
   16.20 +  | string str =
   16.21 +      str |> translate_string (fn ch =>
   16.22 +        let val c = ord ch in
   16.23 +          (case ch of
   16.24 +            "\t" => "$'\\t'"
   16.25 +          | "\n" => "$'\\n'"
   16.26 +          | "\f" => "$'\\f'"
   16.27 +          | "\r" => "$'\\r'"
   16.28 +          | _ =>
   16.29 +              if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
   16.30 +                exists_string (fn c => c = ch) "-./:_" then ch
   16.31 +              else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
   16.32 +              else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
   16.33 +              else "\\" ^ ch)
   16.34 +        end);
   16.35 +
   16.36 +val strings = space_implode " " o map string;
   16.37 +
   16.38 +end;
    17.1 --- a/src/Pure/System/isabelle_system.scala	Tue Oct 18 15:31:08 2016 +0200
    17.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Oct 18 16:03:30 2016 +0200
    17.3 @@ -318,7 +318,7 @@
    17.4    def hostname(): String = bash("hostname -s").check.out
    17.5  
    17.6    def open(arg: String): Unit =
    17.7 -    bash("exec \"$ISABELLE_OPEN\" " + File.bash_string(arg) + " >/dev/null 2>/dev/null &")
    17.8 +    bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
    17.9  
   17.10    def pdf_viewer(arg: Path): Unit =
   17.11      bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
    18.1 --- a/src/Pure/System/isabelle_tool.scala	Tue Oct 18 15:31:08 2016 +0200
    18.2 +++ b/src/Pure/System/isabelle_tool.scala	Tue Oct 18 16:03:30 2016 +0200
    18.3 @@ -89,7 +89,7 @@
    18.4          (args: List[String]) =>
    18.5            {
    18.6              val tool = dir + Path.basic(name)
    18.7 -            val result = Isabelle_System.bash(File.bash_path(tool) + " " + File.bash_args(args))
    18.8 +            val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
    18.9              sys.exit(result.print_stdout.rc)
   18.10            }
   18.11      })
    19.1 --- a/src/Pure/Tools/ml_process.scala	Tue Oct 18 15:31:08 2016 +0200
    19.2 +++ b/src/Pure/Tools/ml_process.scala	Tue Oct 18 16:03:30 2016 +0200
    19.3 @@ -107,7 +107,7 @@
    19.4  
    19.5      Bash.process(
    19.6        "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
    19.7 -        File.bash_args(bash_args),
    19.8 +        Bash.strings(bash_args),
    19.9        cwd = cwd,
   19.10        env =
   19.11          Isabelle_System.library_path(env ++ env_options ++ env_tmp,