# HG changeset patch
# User wenzelm
# Date 1669403874 -3600
# Node ID 2590980401b071f33fd90094f3595203daf3e767
# Parent  c9e1276f0268d8bdf24293f449f0f208700a31f1
proper treatment of tar.gz double-extension;

diff -r c9e1276f0268 -r 2590980401b0 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Nov 25 16:20:14 2022 +0100
+++ b/src/Pure/General/file.scala	Fri Nov 25 20:17:54 2022 +0100
@@ -83,6 +83,7 @@
   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_gz(s: String): Boolean = s.endsWith(".tar.gz")
   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 c9e1276f0268 -r 2590980401b0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Fri Nov 25 16:20:14 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala	Fri Nov 25 20:17:54 2022 +0100
@@ -433,14 +433,16 @@
     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 extract(archive: Path, dir: Path): Unit = {
+    val name = archive.file_name
+    if (File.is_zip(name)) {
+      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 error("Cannot extract " + archive)
+  }
 
   def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
     with_tmp_file("patch") { patch =>