# HG changeset patch
# User wenzelm
# Date 1669379895 -3600
# Node ID ded37aade88e6391c24e732fae20cb87c9c9ad86
# Parent  bf537a75e872ee05a4a7564dd33c21c802fca09e
clarified signature;
tuned messages;

diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -96,10 +96,10 @@
       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_name = File.get_dir(tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = archive_name)
 
       Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
         cwd = component_dir.path.file).check
 
 
@@ -107,21 +107,20 @@
 
       progress.echo("Building CSDP for " + platform_name + " ...")
 
-      val build_dir = tmp_dir + Path.basic(source_name)
       build_flags.find(flags => flags.platform == platform_name) match {
         case None => error("No build flags for platform " + quote(platform_name))
         case Some(flags) =>
-          File.find_files(build_dir.file, pred = file => file.getName == "Makefile").
+          File.find_files(source_dir.file, pred = file => file.getName == "Makefile").
             foreach(file => flags.change(File.path(file)))
       }
 
-      progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check
+      progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
 
 
       /* install */
 
-      Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
-      Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
+      Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
+      Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
 
       if (Platform.is_windows) {
         Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw,
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_easychair.scala
--- a/src/Pure/Admin/build_easychair.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -30,13 +30,7 @@
         Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
           cwd = download_dir.file).check
 
-        val easychair_dir =
-          File.read_dir(download_dir) match {
-            case List(name) => download_dir + Path.explode(name)
-            case bad =>
-              error("Expected exactly one directory entry in " + download_file +
-                bad.mkString("\n", "\n  ", ""))
-          }
+        val easychair_dir = File.get_dir(download_dir, title = download_url)
 
 
         /* component */
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_foiltex.scala
--- a/src/Pure/Admin/build_foiltex.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -30,13 +30,7 @@
         Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
           cwd = download_dir.file).check
 
-        val foiltex_dir =
-          File.read_dir(download_dir) match {
-            case List(name) => download_dir + Path.explode(name)
-            case bad =>
-              error("Expected exactly one directory entry in " + download_file +
-                bad.mkString("\n", "\n  ", ""))
-          }
+        val foiltex_dir = File.get_dir(download_dir, title = download_url)
 
         val README = Path.explode("README")
         val README_flt = Path.explode("README.flt")
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -121,13 +121,8 @@
         Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
       }
 
-      val dir_entry =
-        File.read_dir(tmp_dir) match {
-          case List(s) => s
-          case _ => error("Archive contains multiple directories")
-        }
+      val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name)
 
-      val jdk_dir = tmp_dir + Path.explode(dir_entry)
       val platform =
         templates.view.flatMap(_.detect(jdk_dir))
           .headOption.getOrElse(error("Failed to detect JDK platform"))
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_llncs.scala
--- a/src/Pure/Admin/build_llncs.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -33,13 +33,7 @@
         Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
           cwd = download_dir.file).check
 
-        val llncs_dir =
-          File.read_dir(download_dir) match {
-            case List(name) => download_dir + Path.explode(name)
-            case bad =>
-              error("Expected exactly one directory entry in " + download_file +
-                bad.mkString("\n", "\n  ", ""))
-          }
+        val llncs_dir = File.get_dir(download_dir, title = download_url)
 
         val readme = Path.explode("README.md")
         File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_minisat.scala
--- a/src/Pure/Admin/build_minisat.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_minisat.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -61,10 +61,10 @@
       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_name = File.get_dir(tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = download_url)
 
       Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
         cwd = component_dir.path.file).check
 
 
@@ -72,18 +72,17 @@
 
       progress.echo("Building Minisat for " + platform_name + " ...")
 
-      val build_dir = tmp_dir + Path.basic(source_name)
-      Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+      Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
 
       if (Platform.is_macos) {
-        File.change(build_dir + Path.explode("Makefile")) {
+        File.change(source_dir + Path.explode("Makefile")) {
           _.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
         }
       }
-      progress.bash("make r", build_dir.file, echo = verbose).check
+      progress.bash("make r", source_dir.file, echo = verbose).check
 
       Isabelle_System.copy_file(
-        build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
+        source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
 
       if (Platform.is_windows) {
         Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir)
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_vampire.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -66,10 +66,10 @@
       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_name = File.get_dir(tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = download_url)
 
       Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
         cwd = component_dir.path.file).check
 
 
@@ -77,22 +77,21 @@
 
       progress.echo("Building Vampire for " + platform_name + " ...")
 
-      val build_dir = tmp_dir + Path.basic(source_name)
-      Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir.path)
+      Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path)
 
       val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
       val cmake_out =
         progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
-          cwd = build_dir.file, echo = verbose).check.out
+          cwd = source_dir.file, echo = verbose).check.out
 
       val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
       val binary =
         split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
           .getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
 
-      progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
+      progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
 
-      Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+      Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
         platform_dir + Path.basic("vampire").platform_exe)
 
 
diff -r bf537a75e872 -r ded37aade88e src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Admin/build_verit.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -62,10 +62,10 @@
       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_name = File.get_dir(tmp_dir)
+      val source_dir = File.get_dir(tmp_dir, title = download_url)
 
       Isabelle_System.bash(
-        "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
+        "tar xzf " + archive_path + " && mv " + File.bash_path(source_dir.base) + " src",
         cwd = component_dir.path.file).check
 
 
@@ -76,17 +76,16 @@
       val configure_options =
         if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
 
-      val build_dir = tmp_dir + Path.basic(source_name)
       progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
-        cwd = build_dir.file, echo = verbose).check
+        cwd = source_dir.file, echo = verbose).check
 
 
       /* install */
 
-      Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+      Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
 
       val exe_path = Path.basic("veriT").platform_exe
-      Isabelle_System.copy_file(build_dir + exe_path, platform_dir)
+      Isabelle_System.copy_file(source_dir + exe_path, platform_dir)
       Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
 
 
diff -r bf537a75e872 -r ded37aade88e src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/file.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -128,13 +128,26 @@
     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 get_entry(
+    dir: Path,
+    pred: Path => Boolean = _ => true,
+    title: String = ""
+  ): Path =
+    read_dir(dir).filter(name => pred(dir + Path.basic(name))) match {
+      case List(entry) => dir + Path.basic(entry)
+      case bad =>
+        error("Bad directory content in " + (if (title.nonEmpty) title else dir.toString) +
+          "\nexpected a single entry, but found" +
+          (if (bad.isEmpty) " nothing"
+           else bad.sorted.map(quote).mkString(":\n  ", "\n  ", "")))
     }
 
+  def get_file(dir: Path, title: String = ""): Path =
+    get_entry(dir, pred = _.is_file, title = title)
+
+  def get_dir(dir: Path, title: String = ""): Path =
+    get_entry(dir, pred = _.is_dir, title = title)
+
   def find_files(
     start: JFile,
     pred: JFile => Boolean = _ => true,
diff -r bf537a75e872 -r ded37aade88e src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/sql.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -367,11 +367,8 @@
 
   lazy val init_jdbc: Unit = {
     val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform)
-    val lib_name =
-      File.find_files(lib_path.file) match {
-        case List(file) => file.getName
-        case _ => error("Exactly one file expected in directory " + lib_path.expand)
-      }
+    val lib_name = File.get_file(lib_path).file_name
+
     System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
     System.setProperty("org.sqlite.lib.name", lib_name)
 
diff -r bf537a75e872 -r ded37aade88e src/Pure/General/zstd.scala
--- a/src/Pure/General/zstd.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/General/zstd.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -18,12 +18,9 @@
       "Zstd library already initialized by other means than isabelle.Zstd.init()")
 
     val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
-    val lib_file =
-      File.find_files(lib_dir.file) match {
-        case List(file) => file
-        case _ => error("Exactly one file expected in directory " + lib_dir.expand)
-      }
-    System.load(File.platform_path(lib_file.getAbsolutePath))
+    val lib_file = File.get_file(lib_dir)
+
+    System.load(lib_file.absolute_file.getPath)
 
     zstd.util.Native.assumeLoaded()
     assert(zstd.util.Native.isLoaded())
diff -r bf537a75e872 -r ded37aade88e src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Fri Nov 25 10:57:38 2022 +0100
+++ b/src/Pure/Tools/phabricator.scala	Fri Nov 25 13:38:15 2022 +0100
@@ -205,7 +205,7 @@
         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))
+      val build_dir = File.get_dir(tmp_dir, title = mercurial_source)
 
       progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
     }