mkdir_leaf -- avoiding surprises with typos in user-given paths
authorhaftmann
Wed, 30 Jun 2010 12:20:45 +0200
changeset 37651 62fc16341922
parent 37641 39bd6f7c25c2
child 37652 6aa09d2a6cf9
mkdir_leaf -- avoiding surprises with typos in user-given paths
src/Pure/General/file.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_scala.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));
 
--- 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)
--- 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