src/Pure/General/file.ML
author wenzelm
Sat, 16 Jul 2011 18:41:35 +0200
changeset 43848 8f2bf02a0ccb
parent 43845 d89353d17f54
child 44879 3b6613366dd7
permissions -rw-r--r--
some file and directory operations;
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
    Author:     Markus Wenzel, TU Muenchen
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     3
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     4
File system operations.
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     5
*)
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
signature FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
     8
sig
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
     9
  val platform_path: Path.T -> string
32943
2cb928848e77 exported File.shell_quote;
wenzelm
parents: 32738
diff changeset
    10
  val shell_quote: string -> string
16261
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
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    14
  val full_path: Path.T -> Path.T -> Path.T
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    15
  val tmp_path: Path.T -> Path.T
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    16
  val exists: Path.T -> bool
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    17
  val rm: Path.T -> unit
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    18
  val is_dir: Path.T -> bool
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    19
  val check_dir: Path.T -> Path.T
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    20
  val check_file: Path.T -> Path.T
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
    21
  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    22
  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
    23
  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
    24
  val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
    25
  val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
    26
  val read_dir: Path.T -> string list
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    27
  val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
43845
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
    28
  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
    29
  val read_lines: Path.T -> string list
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    30
  val read: Path.T -> string
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    31
  val write: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    32
  val append: Path.T -> string -> unit
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    33
  val write_list: Path.T -> string list -> unit
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    34
  val append_list: Path.T -> string list -> unit
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    35
  val write_buffer: Path.T -> Buffer.T -> unit
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
    36
  val eq: Path.T * Path.T -> bool
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    37
  val copy: Path.T -> Path.T -> unit
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    38
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    39
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    40
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    41
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    42
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    43
(* system path representations *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    44
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    45
val platform_path = Path.implode o Path.expand;
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    46
40746
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    47
fun shell_quote s =
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    48
  if exists_string (fn c => c = "'") s then
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    49
    error ("Illegal single quote in path specification: " ^ quote s)
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    50
  else enclose "'" "'" s;
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    51
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    52
val shell_path = shell_quote o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    53
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    54
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    55
(* current working directory *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    56
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    57
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
    58
val pwd = Path.explode o pwd;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    59
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    60
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    61
(* full_path *)
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    62
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    63
fun full_path dir path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    64
  let
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    65
    val path' = Path.expand path;
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    66
    val _ = Path.is_current path' andalso error "Bad file specification";
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    67
    val path'' = Path.append dir path';
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    68
  in
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    69
    if Path.is_absolute path'' then path''
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    70
    else Path.append (pwd ()) path''
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    71
  end;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    72
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    73
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    74
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    75
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    76
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    77
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    78
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    79
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    80
(* directory entries *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    81
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    82
val exists = can OS.FileSys.modTime o platform_path;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    83
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    84
val rm = OS.FileSys.remove o platform_path;
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    85
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    86
fun is_dir path =
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    87
  the_default false (try OS.FileSys.isDir (platform_path path));
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    88
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    89
fun check_dir path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    90
  if exists path andalso is_dir path then path
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    91
  else error ("No such directory: " ^ Path.print path);
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    92
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    93
fun check_file path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    94
  if exists path andalso not (is_dir path) then path
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    95
  else error ("No such file: " ^ Path.print path);
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    96
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    97
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
    98
(* open streams *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    99
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   100
local
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   101
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   102
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
   103
  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
   104
  in Exn.release (Exn.capture f file before close_file file) end;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   105
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   106
in
6218
3e9d6edc99a8 added join_info;
wenzelm
parents: 6182
diff changeset
   107
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   108
fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   109
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
   110
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
   111
fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   112
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   113
end;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   114
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   115
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   116
(* directory content *)
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   117
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   118
fun fold_dir f path a = open_dir (fn stream =>
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   119
  let
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   120
    fun read x =
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   121
      (case OS.FileSys.readDir stream of
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   122
        NONE => x
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   123
      | SOME entry => read (f entry x));
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   124
  in read a end) path;
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   125
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   126
fun read_dir path = rev (fold_dir cons path []);
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   127
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   128
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   129
(* input *)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   130
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   131
(*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
43845
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
   132
fun fold_chunks terminator f path a = open_input (fn file =>
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   133
  let
28510
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   134
    fun read buf x =
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   135
      (case TextIO.input file of
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   136
        "" => (case Buffer.content buf of "" => x | line => f line x)
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   137
      | input =>
43845
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
   138
          (case String.fields (fn c => c = terminator) input of
28510
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   139
            [rest] => read (Buffer.add rest buf) x
43616
9e237a9dc1fd reverted 782991e4180d: fold_fields was never used
noschinl
parents: 42329
diff changeset
   140
          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
9e237a9dc1fd reverted 782991e4180d: fold_fields was never used
noschinl
parents: 42329
diff changeset
   141
    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
9e237a9dc1fd reverted 782991e4180d: fold_fields was never used
noschinl
parents: 42329
diff changeset
   142
      | read_lines (line :: more) x = read_lines more (f line x);
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   143
  in read Buffer.empty a end) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   144
43845
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
   145
fun fold_lines f = fold_chunks #"\n" f;
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
   146
fun fold_pages f = fold_chunks #"\f" f;
d89353d17f54 added File.fold_pages for streaming of large files;
wenzelm
parents: 43616
diff changeset
   147
43848
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   148
fun read_lines path = rev (fold_lines cons path []);
8f2bf02a0ccb some file and directory operations;
wenzelm
parents: 43845
diff changeset
   149
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   150
val read = open_input TextIO.inputAll;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   151
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   152
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   153
(* output *)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   154
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   155
fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   156
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   157
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
   158
fun append_list path txts = open_append (output txts) path;
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   159
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   160
fun write path txt = write_list path [txt];
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   161
fun append path txt = append_list path [txt];
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   162
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   163
fun write_buffer path buf = open_output (Buffer.output buf) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   164
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   165
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   166
(* copy *)
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   167
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   168
fun eq paths =
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   169
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
26656
62fff5feb756 Library.is_equal;
wenzelm
parents: 26503
diff changeset
   170
    SOME ids => is_equal (OS.FileSys.compare ids)
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   171
  | NONE => false);
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   172
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   173
fun copy src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   174
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   175
  else
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   176
    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
   177
    in write target (read src) end;
6318
4a423e8a0b54 added mkdir;
wenzelm
parents: 6224
diff changeset
   178
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   179
end;