tuned;
authorwenzelm
Sat, 05 Mar 2022 10:55:48 +0100
changeset 75218 05a2586ec89a
parent 75217 6e7b3492d7df
child 75219 6d1b64d76b57
tuned;
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 **/