# HG changeset patch
# User wenzelm
# Date 1669817011 -3600
# Node ID 83de6e9ae9831d0c4c8968885c907f24a68f8beb
# Parent  8c94ca4dd035953eea71755ef59ab446b034bca1
clarified signature: prefer Scala functions instead of shell scripts;

diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_csdp.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -95,12 +95,11 @@
       val archive_path = tmp_dir + Path.basic(archive_name)
       Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
-      val source_dir = File.get_dir(tmp_dir, title = archive_name)
+      Isabelle_System.extract(archive_path, tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = download_url)
 
-      Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_e.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -41,35 +41,35 @@
       val archive_path = tmp_dir + Path.explode("E.tgz")
       Isabelle_System.download_file(archive_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
-      Isabelle_System.bash("tar xzf " + archive_path + " && mv E src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = archive_url)
+
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
 
       progress.echo("Building E prover for " + platform_name + " ...")
 
-      val build_dir = tmp_dir + Path.basic("E")
       val build_options = {
-        val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
+        val result = Isabelle_System.bash("./configure --help", cwd = source_dir.file)
         if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
       }
 
       val build_script = "./configure" + build_options + " && make"
-      Isabelle_System.bash(build_script,
-        cwd = build_dir.file,
+      Isabelle_System.bash(build_script, cwd = source_dir.file,
         progress_stdout = progress.echo_if(verbose, _),
         progress_stderr = progress.echo_if(verbose, _)).check
 
 
       /* install */
 
-      Isabelle_System.copy_file(build_dir + Path.basic("COPYING"), component_dir.LICENSE)
+      Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE)
 
       val install_files = List("epclextract", "eprover", "eprover-ho")
       for (name <- install_files ::: install_files.map(_ + ".exe")) {
-        val path = build_dir + Path.basic("PROVER") + Path.basic(name)
+        val path = source_dir + Path.basic("PROVER") + Path.basic(name)
         if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
       }
       Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_jedit.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -143,7 +143,7 @@
         File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
 
       val source_path = download_jedit(tmp_dir, "source.tar.bz2")
-      Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
+      Isabelle_System.extract(source_path, jedit_dir)
 
 
       /* patched version */
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_lipics.scala
--- a/src/Pure/Admin/build_lipics.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_lipics.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -36,8 +36,7 @@
         /* download */
 
         Isabelle_System.download_file(download_url, download_file, progress = progress)
-        Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
-          dir = download_dir, strip = 1).check
+        Isabelle_System.extract(download_file, download_dir, strip = true)
 
         val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
 
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_minisat.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -60,12 +60,11 @@
       val archive_path = tmp_dir + Path.basic(archive_name)
       Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+      Isabelle_System.extract(archive_path, tmp_dir)
       val source_dir = File.get_dir(tmp_dir, title = download_url)
 
-      Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_release.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -13,7 +13,7 @@
   private def execute(dir: Path, script: String): Unit =
     Isabelle_System.bash(script, cwd = dir.file).check
 
-  private def execute_tar(dir: Path, args: String, strip: Int = 0): Process_Result =
+  private def execute_tar(dir: Path, args: String, strip: Boolean = false): Process_Result =
     Isabelle_System.gnutar(args, dir = dir, strip = strip).check
 
   private def bash_java_opens(args: String*): String =
@@ -107,7 +107,7 @@
           val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
 
           Bytes.write(archive_path, bytes)
-          execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
+          execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = true)
 
           val id = File.read(isabelle_dir + ISABELLE_ID)
           val tags = File.read(isabelle_dir + ISABELLE_TAGS)
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_scala.scala
--- a/src/Pure/Admin/build_scala.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_scala.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -28,12 +28,11 @@
     def get(path: Path, progress: Progress = new Progress): Unit =
       Isabelle_System.download_file(proper_url, path, progress = progress)
 
-    def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
-      Isabelle_System.with_tmp_file("archive"){ archive_path =>
+    def get_unpacked(dir: Path, strip: Boolean = false, progress: Progress = new Progress): Unit =
+      Isabelle_System.with_tmp_file("archive", ext = "tar.gz"){ archive_path =>
         get(archive_path, progress = progress)
         progress.echo("Unpacking " + artifact)
-        Isabelle_System.gnutar(
-          "-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
+        Isabelle_System.extract(archive_path, dir, strip = strip)
       }
 
     def print: String =
@@ -77,7 +76,7 @@
 
     /* download */
 
-    main_download.get_unpacked(component_dir.path, strip = 1, progress = progress)
+    main_download.get_unpacked(component_dir.path, strip = true, progress = progress)
 
     lib_downloads.foreach(download =>
       download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_spass.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -29,9 +29,9 @@
       val Component_Name = """^(.+)-src\.tar.gz$""".r
       val Version = """^[^-]+-([^-]+)$""".r
 
-      val (archive_name, archive_base_name) =
+      val archive_name =
         download_url match {
-          case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", name))
+          case Archive_Name(name) => name
           case _ => error("Failed to determine source archive name from " + quote(download_url))
         }
 
@@ -67,38 +67,36 @@
       val archive_path = tmp_dir + Path.basic(archive_name)
       Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
-      Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = download_url)
+
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
 
       progress.echo("Building SPASS for " + platform_name + " ...")
 
-      val build_dir = tmp_dir + Path.basic(archive_base_name)
-
       if (Platform.is_windows) {
-        File.change(build_dir + Path.basic("misc.c")) {
+        File.change(source_dir + Path.basic("misc.c")) {
           _.replace("""#include "execinfo.h" """, "")
            .replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
         }
       }
 
-      Isabelle_System.bash("make",
-        cwd = build_dir.file,
+      Isabelle_System.bash("make", cwd = source_dir.file,
         progress_stdout = progress.echo_if(verbose, _),
         progress_stderr = progress.echo_if(verbose, _)).check
 
 
       /* install */
 
-      Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), component_dir.LICENSE)
+      Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE)
 
       val install_files = List("SPASS")
       for (name <- install_files ::: install_files.map(_ + ".exe")) {
-        val path = build_dir + Path.basic(name)
+        val path = source_dir + Path.basic(name)
         if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
       }
 
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_vampire.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -65,12 +65,11 @@
       val archive_path = tmp_dir + Path.basic(archive_name)
       Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+      Isabelle_System.extract(archive_path, tmp_dir)
       val source_dir = File.get_dir(tmp_dir, title = download_url)
 
-      Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Admin/build_verit.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -61,12 +61,11 @@
       val archive_path = tmp_dir + Path.basic(archive_name)
       Isabelle_System.download_file(download_url, archive_path, progress = progress)
 
-      Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+      Isabelle_System.extract(archive_path, tmp_dir)
       val source_dir = File.get_dir(tmp_dir, title = download_url)
 
-      Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_path, component_dir.path)
+      Isabelle_System.move_file(component_dir.path + source_dir.base, component_dir.src)
 
 
       /* build */
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/General/file.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -83,7 +83,9 @@
   def is_node(s: String): Boolean = s.endsWith(".node")
   def is_pdf(s: String): Boolean = s.endsWith(".pdf")
   def is_png(s: String): Boolean = s.endsWith(".png")
+  def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
   def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
+  def is_tgz(s: String): Boolean = s.endsWith(".tgz")
   def is_thy(s: String): Boolean = s.endsWith(".thy")
   def is_xz(s: String): Boolean = s.endsWith(".xz")
   def is_zip(s: String): Boolean = s.endsWith(".zip")
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/General/mercurial.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -74,7 +74,7 @@
         Bytes.write(archive_path, content.bytes)
         progress.echo("Unpacking " + rev + ".tar.gz")
         Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
-          dir = dir, original_owner = true, strip = 1).check
+          dir = dir, original_owner = true, strip = true).check
       }
     }
   }
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/System/components.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -48,7 +48,7 @@
   def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
     val name = Archive.get_name(archive.file_name)
     progress.echo("Unpacking " + name)
-    Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+    Isabelle_System.extract(archive, dir)
     name
   }
 
@@ -271,7 +271,7 @@
             // contrib directory
             val is_standard_component =
               Isabelle_System.with_tmp_dir("component") { tmp_dir =>
-                Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+                Isabelle_System.extract(archive, tmp_dir)
                 Directory(tmp_dir + Path.explode(name)).check
               }
             if (is_standard_component) {
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/System/isabelle_system.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -421,25 +421,27 @@
     args: String,
     dir: Path = Path.current,
     original_owner: Boolean = false,
-    strip: Int = 0,
+    strip: Boolean = false,
     redirect: Boolean = false
   ): Process_Result = {
     val options =
       (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
       (if (original_owner) "" else "--owner=root --group=staff ") +
-      (if (strip <= 0) "" else "--strip-components=" + strip + " ")
+      (if (!strip) "" else "--strip-components=1 ")
 
     if (gnutar_check) bash("tar " + options + args, redirect = redirect)
     else error("Expected to find GNU tar executable")
   }
 
-  def extract(archive: Path, dir: Path): Unit = {
+  def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = {
     val name = archive.file_name
     if (File.is_zip(name)) {
+      require(!strip, "Cannot use unzip with strip")
       Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
     }
-    else if (File.is_tar_gz(name)) {
-      Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+    else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) {
+      val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf "
+      Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check
     }
     else error("Cannot extract " + archive)
   }
diff -r 8c94ca4dd035 -r 83de6e9ae983 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Mon Nov 28 11:38:55 2022 +0000
+++ b/src/Pure/Tools/phabricator.scala	Wed Nov 30 15:03:31 2022 +0100
@@ -204,7 +204,7 @@
         }
         else Path.explode(mercurial_source)
 
-      Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+      Isabelle_System.extract(archive, tmp_dir)
       val build_dir = File.get_dir(tmp_dir, title = mercurial_source)
 
       progress.bash("make all && make install", cwd = build_dir.file, echo = true).check