--- 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"))
--- 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)
--- 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 */
--- 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