# HG changeset patch
# User wenzelm
# Date 1602417692 -7200
# Node ID 90868036d693961452007d9b6b261b04ff5df7f2
# Parent  a3257d0e8bbbfd10f90134b85fe00effb3bdec23
clarified signature;

diff -r a3257d0e8bbb -r 90868036d693 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sun Oct 11 13:50:19 2020 +0200
+++ b/src/Pure/Admin/build_csdp.scala	Sun Oct 11 14:01:32 2020 +0200
@@ -100,14 +100,8 @@
       Isabelle_System.download(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+      val source_name = File.get_dir(tmp_dir)
 
-      val source_name =
-        File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match {
-          case List(dir) => dir
-          case dirs =>
-            error("Exactly one directory entry expected in archive " + quote(download_url) +
-              "\n" + commas_quote(dirs))
-        }
       Isabelle_System.bash(
         "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
         cwd = component_dir.file).check
diff -r a3257d0e8bbb -r 90868036d693 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Sun Oct 11 13:50:19 2020 +0200
+++ b/src/Pure/Admin/build_verit.scala	Sun Oct 11 14:01:32 2020 +0200
@@ -82,14 +82,8 @@
       Isabelle_System.download(download_url, archive_path, progress = progress)
 
       Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
+      val source_name = File.get_dir(tmp_dir)
 
-      val source_name =
-        File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match {
-          case List(dir) => dir
-          case dirs =>
-            error("Exactly one directory entry expected in archive " + quote(download_url) +
-              "\n" + commas_quote(dirs))
-        }
       Isabelle_System.bash(
         "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
         cwd = component_dir.file).check
diff -r a3257d0e8bbb -r 90868036d693 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Oct 11 13:50:19 2020 +0200
+++ b/src/Pure/General/file.scala	Sun Oct 11 14:01:32 2020 +0200
@@ -146,6 +146,13 @@
     else files.toList.map(_.getName).sorted
   }
 
+  def get_dir(dir: Path): String =
+    read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
+      case List(entry) => entry
+      case dirs =>
+        error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
+    }
+
   def find_files(
     start: JFile,
     pred: JFile => Boolean = _ => true,
diff -r a3257d0e8bbb -r 90868036d693 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Sun Oct 11 13:50:19 2020 +0200
+++ b/src/Pure/Tools/phabricator.scala	Sun Oct 11 14:01:32 2020 +0200
@@ -207,15 +207,9 @@
         else Path.explode(mercurial_source)
 
       Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
+      val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir))
 
-      File.read_dir(tmp_dir).filter(name => (tmp_dir + Path.basic(name)).is_dir) match {
-        case List(dir) =>
-          val build_dir = tmp_dir + Path.basic(dir)
-          progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
-        case dirs =>
-          error("Bad archive " + archive +
-            (if (dirs.isEmpty) "" else "\nmultiple directory entries " + commas_quote(dirs)))
-      }
+      progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
     })
   }