--- 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 **/