diff -r 8ae2f8ebc373 -r 87403fde8cc3 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Feb 27 16:33:16 2021 +0100 +++ b/src/Pure/System/isabelle_system.scala Sat Feb 27 17:25:54 2021 +0100 @@ -191,13 +191,17 @@ def make_directory(path: Path): Path = { - if (!path.is_dir) { - bash("perl -e \"use File::Path make_path; make_path('" + File.standard_path(path) + "');\"") - if (!path.is_dir) error("Failed to create directory: " + path.absolute) - } + try { Files.createDirectories(path.file.toPath) } + catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } path } + object Make_Directory extends Scala.Fun("make_directory") + { + val here = Scala_Project.here + def apply(arg: String): String = { make_directory(Path.explode(arg)); "" } + } + def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path)