more uniform Isabelle_System.mkdirs in ML/Scala;
authorwenzelm
Sat, 11 Apr 2015 20:00:05 +0200
changeset 60013 42d34eeb283c
parent 60012 0c307c5c03f0
child 60014 e26f9df07530
more uniform Isabelle_System.mkdirs in ML/Scala; avoid odd permission problems on Windows (e.g. Desktop) by using "mkdirs" from Cygwin;
src/Pure/System/isabelle_system.ML
src/Pure/System/isabelle_system.scala
--- 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)
   }