mkdir_leaf -- avoiding surprises with typos in user-given paths
authorhaftmann
Wed Jun 30 12:20:45 2010 +0200 (2010-06-30)
changeset 3765162fc16341922
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
     1.1 --- a/src/Pure/General/file.ML	Wed Jun 30 11:39:10 2010 +0200
     1.2 +++ b/src/Pure/General/file.ML	Wed Jun 30 12:20:45 2010 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val check: Path.T -> unit
     1.5    val rm: Path.T -> unit
     1.6    val mkdir: Path.T -> unit
     1.7 +  val mkdir_leaf: Path.T -> unit
     1.8    val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
     1.9    val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
    1.10    val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
    1.11 @@ -135,6 +136,8 @@
    1.12  
    1.13  fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
    1.14  
    1.15 +fun mkdir_leaf path = system_command ("mkdir " ^ shell_path path);
    1.16 +
    1.17  fun is_dir path =
    1.18    the_default false (try OS.FileSys.isDir (platform_path path));
    1.19  
     2.1 --- a/src/Tools/Code/code_haskell.ML	Wed Jun 30 11:39:10 2010 +0200
     2.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Jun 30 12:20:45 2010 +0200
     2.3 @@ -382,7 +382,7 @@
     2.4            | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
     2.5                  o Long_Name.explode) modlname;
     2.6          val pathname = Path.append destination filename;
     2.7 -        val _ = File.mkdir (Path.dir pathname);
     2.8 +        val _ = File.mkdir_leaf (Path.dir pathname);
     2.9        in File.write pathname
    2.10          ("{-# OPTIONS_GHC -fglasgow-exts #-}\n\n"
    2.11            ^ code_of_pretty content)
     3.1 --- a/src/Tools/Code/code_scala.ML	Wed Jun 30 11:39:10 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Wed Jun 30 12:20:45 2010 +0200
     3.3 @@ -376,7 +376,7 @@
     3.4            | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
     3.5                  o Long_Name.explode) modlname;
     3.6          val pathname = Path.append destination filename;
     3.7 -        val _ = File.mkdir (Path.dir pathname);
     3.8 +        val _ = File.mkdir_leaf (Path.dir pathname);
     3.9        in File.write pathname (code_of_pretty content) end
    3.10    in
    3.11      Code_Target.mk_serialization target NONE