1.1 --- a/src/Pure/General/file.ML	Sun Nov 28 16:15:31 2010 +0100
     1.2 +++ b/src/Pure/General/file.ML	Sun Nov 28 16:35:56 2010 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4    val exists: Path.T -> bool
     1.5    val check: Path.T -> unit
     1.6    val rm: Path.T -> unit
     1.7 +  val is_dir: Path.T -> bool
     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 @@ -71,6 +72,9 @@
    1.12  
    1.13  val rm = OS.FileSys.remove o platform_path;
    1.14  
    1.15 +fun is_dir path =
    1.16 +  the_default false (try OS.FileSys.isDir (platform_path path));
    1.17 +
    1.18  
    1.19  (* open files *)
    1.20  
    1.21 @@ -128,9 +132,6 @@
    1.22      SOME ids => is_equal (OS.FileSys.compare ids)
    1.23    | NONE => false);
    1.24  
    1.25 -fun is_dir path =
    1.26 -  the_default false (try OS.FileSys.isDir (platform_path path));
    1.27 -
    1.28  fun copy src dst =
    1.29    if eq (src, dst) then ()
    1.30    else

     2.1 --- a/src/Pure/System/isabelle_system.ML	Sun Nov 28 16:15:31 2010 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.ML	Sun Nov 28 16:35:56 2010 +0100
     2.3 @@ -41,7 +41,8 @@
     2.4  
     2.5  fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
     2.6  
     2.7 -val mkdir = OS.FileSys.mkDir o File.platform_path;
     2.8 +fun mkdir path =
     2.9 +  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
    2.10  
    2.11  fun copy_dir src dst =
    2.12    if File.eq (src, dst) then ()