# HG changeset patch
# User wenzelm
# Date 1669383862 -3600
# Node ID 2bf13b30b98e84f493d694860c1a6b0ff1d39c10
# Parent  ded37aade88e6391c24e732fae20cb87c9c9ad86
clarified signature;
omit somewhat pointless test for "unzip" command;

diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_easychair.scala
--- a/src/Pure/Admin/build_easychair.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -19,16 +19,13 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.require_command("unzip", test = "-h")
-
     Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
       Isabelle_System.with_tmp_dir("download") { download_dir =>
 
         /* download */
 
         Isabelle_System.download_file(download_url, download_file, progress = progress)
-        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
-          cwd = download_dir.file).check
+        Isabelle_System.extract(download_file, download_dir)
 
         val easychair_dir = File.get_dir(download_dir, title = download_url)
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_eptcs.scala
--- a/src/Pure/Admin/build_eptcs.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_eptcs.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -23,9 +23,6 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.require_command("unzip", test = "-h")
-
-
     /* component */
 
     val component = "eptcs-" + version
@@ -39,8 +36,7 @@
 
     Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
       Isabelle_System.download_file(download_url, download_file, progress = progress)
-      Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(download_file, component_dir.path)
     }
 
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_foiltex.scala
--- a/src/Pure/Admin/build_foiltex.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -19,16 +19,13 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.require_command("unzip", test = "-h")
-
     Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
       Isabelle_System.with_tmp_dir("download") { download_dir =>
 
         /* download */
 
         Isabelle_System.download_file(download_url, download_file, progress = progress)
-        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
-          cwd = download_dir.file).check
+        Isabelle_System.extract(download_file, download_dir)
 
         val foiltex_dir = File.get_dir(download_dir, title = download_url)
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -113,13 +113,7 @@
     try {
       val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
 
-      if (archive.get_ext == "zip") {
-        Isabelle_System.bash(
-          "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
-      }
-      else {
-        Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
-      }
+      Isabelle_System.extract(archive, tmp_dir)
 
       val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name)
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -111,7 +111,6 @@
   ): Unit = {
     Isabelle_System.require_command("ant", test = "-version")
     Isabelle_System.require_command("patch")
-    Isabelle_System.require_command("unzip", test = "-h")
 
     val component_dir = Components.Directory.create(component_path, progress = progress)
 
@@ -206,7 +205,7 @@
           "https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
             name + "-" + vers + "-bin.zip/download"
         Isabelle_System.download_file(url, zip_path, progress = progress)
-        Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
+        Isabelle_System.extract(zip_path, jars_dir)
       }
     }
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_llncs.scala
--- a/src/Pure/Admin/build_llncs.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -22,16 +22,13 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.require_command("unzip", test = "-h")
-
     Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
       Isabelle_System.with_tmp_dir("download") { download_dir =>
 
         /* download */
 
         Isabelle_System.download_file(download_url, download_file, progress = progress)
-        Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
-          cwd = download_dir.file).check
+        Isabelle_System.extract(download_file, download_dir)
 
         val llncs_dir = File.get_dir(download_dir, title = download_url)
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_pdfjs.scala
--- a/src/Pure/Admin/build_pdfjs.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_pdfjs.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -25,9 +25,6 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.require_command("unzip", test = "-h")
-
-
     /* component name */
 
     val component = "pdfjs-" + version
@@ -41,8 +38,7 @@
     Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
       Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-legacy-dist.zip",
         archive_file, progress = progress)
-      Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
-        cwd = component_dir.path.file).check
+      Isabelle_System.extract(archive_file, component_dir.path)
     }
 
 
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -146,13 +146,7 @@
   /** skeleton for component **/
 
   private def extract_sources(source_archive: Path, component_dir: Path): Unit = {
-    if (source_archive.get_ext == "zip") {
-      Isabelle_System.bash(
-        "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
-    }
-    else {
-      Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
-    }
+    Isabelle_System.extract(source_archive, component_dir)
 
     val src_dir = component_dir + Path.explode("src")
     File.read_dir(component_dir) match {
diff -r ded37aade88e -r 2bf13b30b98e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -433,6 +433,15 @@
     else error("Expected to find GNU tar executable")
   }
 
+  def extract(archive: Path, dir: Path): Unit =
+    archive.get_ext match {
+      case "zip" =>
+        Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
+      case "tar.gz" | "tgz" =>
+        Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+      case _ => error("Cannot extract " + archive)
+    }
+
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
     with_tmp_file("patch") { patch =>
       Isabelle_System.bash(
diff -r ded37aade88e -r 2bf13b30b98e src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Fri Nov 25 13:38:15 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Fri Nov 25 14:44:22 2022 +0100
@@ -69,19 +69,12 @@
     def download_zip: Boolean = File.is_zip(download_name)
 
     def download(dir: Path, progress: Progress = new Progress): Unit = {
-      if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
-
       Isabelle_System.with_tmp_file("download") { download_file =>
         Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
           download_file, progress = progress)
 
         progress.echo("Extract ...")
-        if (download_zip) {
-          Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check
-        }
-        else {
-          Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
-        }
+        Isabelle_System.extract(download_file, dir)
       }
     }