clarified signature;
authorwenzelm
Mon, 12 Oct 2020 16:19:11 +0200
changeset 72455 7bf67a58f54a
parent 72454 549391271e74
child 72456 cd3419427cd3
clarified signature;
src/Pure/Admin/build_polyml.scala
src/Pure/Admin/build_spass.scala
src/Pure/Admin/build_verit.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/Admin/build_polyml.scala	Mon Oct 12 15:58:37 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Mon Oct 12 16:19:11 2020 +0200
@@ -72,9 +72,7 @@
       if (!Platform.is_windows) Isabelle_System.settings()
       else Isabelle_System.settings() + ("MSYS" -> mingw.get_root.expand.implode)
 
-    if (platform.is_linux && !Isabelle_System.bash("chrpath -v").ok) {
-      error("""Missing "chrpath" executable on Linux""")
-    }
+    if (platform.is_linux) Isabelle_System.require_command("chrpath")
 
 
     /* bash */
--- a/src/Pure/Admin/build_spass.scala	Mon Oct 12 15:58:37 2020 +0200
+++ b/src/Pure/Admin/build_spass.scala	Mon Oct 12 16:19:11 2020 +0200
@@ -22,10 +22,7 @@
   {
     Isabelle_System.with_tmp_dir("build")(tmp_dir =>
     {
-      /* required commands */
-
-      List("bison", "flex").foreach(cmd =>
-        if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd))
+      Isabelle_System.require_command("bison", "flex")
 
 
       /* component */
--- a/src/Pure/Admin/build_verit.scala	Mon Oct 12 15:58:37 2020 +0200
+++ b/src/Pure/Admin/build_verit.scala	Mon Oct 12 16:19:11 2020 +0200
@@ -22,10 +22,7 @@
   {
     Isabelle_System.with_tmp_dir("build")(tmp_dir =>
     {
-      /* required commands */
-
-      List("autoconf", "bison", "flex", "wget").foreach(cmd =>
-        if (!Isabelle_System.bash(cmd + " --version").ok) error("Missing command: " + cmd))
+      Isabelle_System.require_command("autoconf", "bison", "flex", "wget")
 
 
       /* component */
--- a/src/Pure/System/isabelle_system.scala	Mon Oct 12 15:58:37 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Oct 12 16:19:11 2020 +0200
@@ -375,9 +375,16 @@
     else error("Expected to find GNU tar executable")
   }
 
+  def require_command(cmds: String*)
+  {
+    for (cmd <- cmds) {
+      if (!bash(Bash.string(cmd) + " --version").ok) error("Missing command: " + quote(cmd))
+    }
+  }
+
   private lazy val curl_check: Unit =
-    try { bash("curl --version").check }
-    catch { case ERROR(_) => error("Cannot download files: missing curl") }
+    try { require_command("curl") }
+    catch { case ERROR(msg) => error(msg + " --- cannot download files") }
 
   def download(url: String, file: Path, progress: Progress = new Progress): Unit =
   {