# HG changeset patch
# User wenzelm
# Date 1428775205 -7200
# Node ID 42d34eeb283c645de7792a327e86d846f9cfb5f9
# Parent  0c307c5c03f0b4e3a13a8aa89f85126147ecba3d
more uniform Isabelle_System.mkdirs in ML/Scala;
avoid odd permission problems on Windows (e.g. Desktop) by using "mkdirs" from Cygwin;

diff -r 0c307c5c03f0 -r 42d34eeb283c src/Pure/System/isabelle_system.ML
--- 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);
diff -r 0c307c5c03f0 -r 42d34eeb283c src/Pure/System/isabelle_system.scala
--- 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)
   }