more uniform Isabelle_System.mkdirs in ML/Scala;
avoid odd permission problems on Windows (e.g. Desktop) by using "mkdirs" from Cygwin;
--- a/src/Pure/System/isabelle_system.ML Sat Apr 11 13:21:40 2015 +0200
+++ b/src/Pure/System/isabelle_system.ML Sat Apr 11 20:00:05 2015 +0200
@@ -58,7 +58,10 @@
(* directory operations *)
-fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
+fun mkdirs path =
+ if #rc (Bash.process ("mkdir -p " ^ File.shell_path path)) <> 0 then
+ error ("Failed to create directory: " ^ Path.print path)
+ else ();
fun mkdir path =
if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
--- a/src/Pure/System/isabelle_system.scala Sat Apr 11 13:21:40 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Apr 11 20:00:05 2015 +0200
@@ -256,11 +256,9 @@
/* mkdirs */
- def mkdirs(path: Path)
- {
- path.file.mkdirs
- if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
- }
+ def mkdirs(path: Path): Unit =
+ if (bash("mkdir -p " + shell_path(path)).rc != 0)
+ error("Failed to create directory: " + quote(platform_path(path)))
@@ -388,7 +386,7 @@
private def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
- mkdirs(path)
+ path.file.mkdirs // low-level mkdirs
platform_file(path)
}