src/Pure/General/file.ML
author wenzelm
Sat, 24 May 2008 14:47:43 +0200
changeset 26980 f7f48bb9a025
parent 26946 0b6eff8c088d
child 28028 c0f54a32491e
permissions -rw-r--r--
ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6118
caa439435666 fixed titles;
wenzelm
parents: 5009
diff changeset
     1
(*  Title:      Pure/General/file.ML
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     4
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     5
File system operations.
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     6
*)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     7
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     8
signature FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     9
sig
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    10
  val platform_path: Path.T -> string
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    11
  val shell_path: Path.T -> string
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    12
  val cd: Path.T -> unit
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    13
  val pwd: unit -> Path.T
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    14
  val full_path: Path.T -> Path.T
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    15
  val tmp_path: Path.T -> Path.T
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    16
  val isatool: string -> int
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    17
  val system_command: string -> unit
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    18
  eqtype ident
23874
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    19
  val rep_ident: ident -> string
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    20
  val ident: Path.T -> ident option
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    21
  val exists: Path.T -> bool
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    22
  val check: Path.T -> unit
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    23
  val rm: Path.T -> unit
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    24
  val mkdir: Path.T -> unit
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    25
  val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    26
  val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    27
  val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    28
  val read: Path.T -> string
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    29
  val write: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    30
  val append: Path.T -> string -> unit
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    31
  val write_list: Path.T -> string list -> unit
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    32
  val append_list: Path.T -> string list -> unit
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
    33
  val eq: Path.T * Path.T -> bool
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    34
  val copy: Path.T -> Path.T -> unit
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    35
  val copy_dir: Path.T -> Path.T -> unit
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    36
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    37
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    38
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    39
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    40
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    41
(* system path representations *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    42
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    43
val platform_path = Path.implode o Path.expand;
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    44
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    45
val shell_quote = enclose "'" "'";
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    46
val shell_path = shell_quote o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    47
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    48
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    49
(* current working directory *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    50
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    51
val cd = cd o platform_path;
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    52
val pwd = Path.explode o pwd;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    53
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    54
fun full_path path =
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
    55
  if Path.is_absolute path then path
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
    56
  else Path.append (pwd ()) path;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    57
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    58
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    59
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    60
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    61
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    62
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    63
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    64
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    65
(* system commands *)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    66
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    67
fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    68
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    69
fun system_command cmd =
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    70
  if system cmd <> 0 then error ("System command failed: " ^ cmd)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    71
  else ();
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    72
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    73
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    74
(* file identification *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    75
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    76
local
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    77
  val ident_cache = ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    78
in
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    79
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    80
fun check_cache (path, time) = CRITICAL (fn () =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    81
  (case Symtab.lookup (! ident_cache) path of
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    82
    NONE => NONE
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    83
  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    84
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    85
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    86
  change ident_cache (Symtab.update (path, {time_stamp = time, id = id})));
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    87
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    88
end;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    89
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    90
datatype ident = Ident of string;
23874
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    91
fun rep_ident (Ident s) = s;
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    92
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    93
fun ident path =
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    94
  let val physical_path = perhaps (try OS.FileSys.fullPath) (platform_path path) in
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    95
    (case try (Time.toString o OS.FileSys.modTime) physical_path of
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
    96
      NONE => NONE
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    97
    | SOME mod_time => SOME (Ident
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
    98
        (case getenv "ISABELLE_FILE_IDENT" of
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    99
          "" => physical_path ^ ": " ^ mod_time
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
   100
        | cmd =>
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   101
            (case check_cache (physical_path, mod_time) of
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   102
              SOME id => id
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   103
            | NONE =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   104
                let val (id, rc) =  (*potentially slow*)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   105
                  system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_quote physical_path)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   106
                in
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   107
                  if id <> "" andalso rc = 0 then (update_cache (physical_path, (mod_time, id)); id)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   108
                  else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   109
                end))))
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
   110
  end;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   111
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   112
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   113
(* directory entries *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   114
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   115
val exists = can OS.FileSys.modTime o platform_path;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   116
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
   117
fun check path =
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   118
  if exists path then ()
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
   119
  else error ("No such file or directory: " ^ quote (Path.implode path));
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   120
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   121
val rm = OS.FileSys.remove o platform_path;
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   122
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   123
fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   124
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   125
fun is_dir path =
19473
wenzelm
parents: 18715
diff changeset
   126
  the_default false (try OS.FileSys.isDir (platform_path path));
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   127
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   128
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   129
(* read / write files *)
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   130
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   131
local
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   132
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   133
fun with_file open_file close_file f path =
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   134
  let val file = open_file path
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   135
  in Exn.release (Exn.capture f file before close_file file) end;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   136
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   137
fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts;
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   138
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   139
in
6218
3e9d6edc99a8 added join_info;
wenzelm
parents: 6182
diff changeset
   140
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   141
fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   142
fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   143
fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   144
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   145
val read = open_input TextIO.inputAll;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   146
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   147
fun write_list path txts = open_output (output txts) path;
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   148
fun append_list path txts = open_append (output txts) path;
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   149
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   150
fun write path txt = write_list path [txt];
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   151
fun append path txt = append_list path [txt];
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   152
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   153
end;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   154
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   155
fun eq paths =
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   156
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
26656
62fff5feb756 Library.is_equal;
wenzelm
parents: 26503
diff changeset
   157
    SOME ids => is_equal (OS.FileSys.compare ids)
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   158
  | NONE => false);
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   159
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   160
fun copy src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   161
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   162
  else
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   163
    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   164
    in write target (read src) end;
6318
4a423e8a0b54 added mkdir;
wenzelm
parents: 6224
diff changeset
   165
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   166
fun copy_dir src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   167
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   168
  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
6640
d2e8342bf5c3 rearranged order of modules;
wenzelm
parents: 6318
diff changeset
   169
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   170
end;