# HG changeset patch # User wenzelm # Date 1646474148 -3600 # Node ID 05a2586ec89afa6def1873ffe091feb169cdc4cc # Parent 6e7b3492d7df825757f97fb083cc9fd6a1ed0047 tuned; diff -r 6e7b3492d7df -r 05a2586ec89a src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Mar 05 10:48:45 2022 +0100 +++ b/src/Pure/System/isabelle_system.scala Sat Mar 05 10:55:48 2022 +0100 @@ -18,7 +18,7 @@ object Isabelle_System { - /* settings */ + /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { @@ -129,6 +129,10 @@ else "" } + def export_isabelle_identifier(isabelle_identifier: String): String = + if (isabelle_identifier == "") "" + else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" + def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = @@ -405,6 +409,14 @@ watchdog = watchdog, strict = strict) } + + /* command-line tools */ + + def require_command(cmd: String, test: String = "--version"): Unit = + { + if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) + } + private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } @@ -425,11 +437,6 @@ 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 = @@ -451,9 +458,6 @@ external } - def export_isabelle_identifier(isabelle_identifier: String): String = - if (isabelle_identifier == "") "" - else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" /** Isabelle resources **/