# HG changeset patch
# User wenzelm
# Date 1601929397 -7200
# Node ID c7741f767e3e1e91d45cf2bd0859ce58323d467f
# Parent  04bce347868838e88426f0b2fa500861ae2ad58f
clarified signature;

diff -r 04bce3478688 -r c7741f767e3e src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Mon Oct 05 22:07:25 2020 +0200
+++ b/src/Pure/Admin/build_e.scala	Mon Oct 05 22:23:17 2020 +0200
@@ -32,12 +32,8 @@
       /* component */
 
       val component_name = "e-" + version
-      val component_dir = target_dir + Path.basic(component_name)
-      if (component_dir.is_dir) error("Component directory already exists: " + component_dir)
-      else {
-        progress.echo("Component " + component_dir)
-        Isabelle_System.make_directory(component_dir)
-      }
+      val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
+      progress.echo("Component " + component_dir)
 
       val platform_name =
         proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
diff -r 04bce3478688 -r c7741f767e3e src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Mon Oct 05 22:07:25 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Mon Oct 05 22:23:17 2020 +0200
@@ -233,10 +233,7 @@
     component_dir: Path,
     sha1_root: Option[Path] = None)
   {
-    if (component_dir.is_file || component_dir.is_dir)
-      error("Component directory already exists: " + component_dir)
-
-    Isabelle_System.make_directory(component_dir)
+    Isabelle_System.new_directory(component_dir)
     extract_sources(source_archive, component_dir)
 
     File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
diff -r 04bce3478688 -r c7741f767e3e src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Mon Oct 05 22:07:25 2020 +0200
+++ b/src/Pure/Admin/build_sqlite.scala	Mon Oct 05 22:23:17 2020 +0200
@@ -26,12 +26,8 @@
 
     /* component */
 
-    val component_dir = target_dir + Path.basic(download_name)
-    if (component_dir.is_dir) error("Component directory already exists: " + component_dir)
-    else {
-      progress.echo("Component " + component_dir)
-      Isabelle_System.make_directory(component_dir)
-    }
+    val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
+    progress.echo("Component " + component_dir)
 
 
     /* README */
diff -r 04bce3478688 -r c7741f767e3e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Oct 05 22:07:25 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Oct 05 22:23:17 2020 +0200
@@ -198,6 +198,10 @@
     path
   }
 
+  def new_directory(path: Path): Path =
+    if (path.is_dir) error("Directory already exists: " + path)
+    else make_directory(path)
+
   def copy_dir(dir1: Path, dir2: Path): Unit =
     bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check