# HG changeset patch
# User haftmann
# Date 1277893245 -7200
# Node ID 62fc163419229c06785aed8c42efd7a0a8bfa075
# Parent  39bd6f7c25c2f57575f81f96b8c25c9432a6e1d7
mkdir_leaf -- avoiding surprises with typos in user-given paths

diff -r 39bd6f7c25c2 -r 62fc16341922 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jun 30 11:39:10 2010 +0200
+++ b/src/Pure/General/file.ML	Wed Jun 30 12:20:45 2010 +0200
@@ -21,6 +21,7 @@
   val check: Path.T -> unit
   val rm: Path.T -> unit
   val mkdir: Path.T -> unit
+  val mkdir_leaf: Path.T -> unit
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -135,6 +136,8 @@
 
 fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
 
+fun mkdir_leaf path = system_command ("mkdir " ^ shell_path path);
+
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));
 
diff -r 39bd6f7c25c2 -r 62fc16341922 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Wed Jun 30 11:39:10 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Jun 30 12:20:45 2010 +0200
@@ -382,7 +382,7 @@
           | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
                 o Long_Name.explode) modlname;
         val pathname = Path.append destination filename;
-        val _ = File.mkdir (Path.dir pathname);
+        val _ = File.mkdir_leaf (Path.dir pathname);
       in File.write pathname
         ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
           ^ code_of_pretty content)
diff -r 39bd6f7c25c2 -r 62fc16341922 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jun 30 11:39:10 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jun 30 12:20:45 2010 +0200
@@ -376,7 +376,7 @@
           | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
                 o Long_Name.explode) modlname;
         val pathname = Path.append destination filename;
-        val _ = File.mkdir (Path.dir pathname);
+        val _ = File.mkdir_leaf (Path.dir pathname);
       in File.write pathname (code_of_pretty content) end
   in
     Code_Target.mk_serialization target NONE