src/Pure/General/file.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28051 56e3a695434f
child 28496 4cff10648928
permissions -rw-r--r--
case default fallback for NBE
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
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    28
  val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    29
  val read: Path.T -> string
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    30
  val write: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    31
  val append: Path.T -> string -> unit
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    32
  val write_list: Path.T -> string list -> unit
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    33
  val append_list: Path.T -> string list -> unit
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    34
  val write_buffer: Path.T -> Buffer.T -> unit
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
    35
  val eq: Path.T * Path.T -> bool
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    36
  val copy: Path.T -> Path.T -> unit
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    37
  val copy_dir: 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
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    47
val shell_quote = enclose "'" "'";
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    48
val shell_path = shell_quote o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    49
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    50
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    51
(* current working directory *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    52
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    53
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
    54
val pwd = Path.explode o pwd;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    55
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    56
fun full_path path =
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
    57
  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
    58
  else Path.append (pwd ()) path;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    59
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    60
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    61
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    62
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    63
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    64
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    65
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    66
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    67
(* system commands *)
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 isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    70
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    71
fun system_command cmd =
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    72
  if system cmd <> 0 then error ("System command failed: " ^ cmd)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    73
  else ();
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    74
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    75
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    76
(* file identification *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    77
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    78
local
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    79
  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
    80
in
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    81
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    82
fun check_cache (path, time) = CRITICAL (fn () =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    83
  (case Symtab.lookup (! ident_cache) path of
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    84
    NONE => NONE
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    85
  | 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
    86
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    87
fun update_cache (path, (time, id)) = CRITICAL (fn () =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    88
  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
    89
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    90
end;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    91
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    92
datatype ident = Ident of string;
23874
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    93
fun rep_ident (Ident s) = s;
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    94
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    95
fun ident path =
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    96
  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
    97
    (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
    98
      NONE => NONE
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    99
    | SOME mod_time => SOME (Ident
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
   100
        (case getenv "ISABELLE_FILE_IDENT" of
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   101
          "" => physical_path ^ ": " ^ mod_time
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
   102
        | cmd =>
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   103
            (case check_cache (physical_path, mod_time) of
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   104
              SOME id => id
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   105
            | NONE =>
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   106
                let val (id, rc) =  (*potentially slow*)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   107
                  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
   108
                in
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   109
                  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
   110
                  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
   111
                end))))
26946
0b6eff8c088d removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
wenzelm
parents: 26656
diff changeset
   112
  end;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   113
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   114
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   115
(* directory entries *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
   116
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   117
val exists = can OS.FileSys.modTime o platform_path;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   118
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
   119
fun check path =
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   120
  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
   121
  else error ("No such file or directory: " ^ quote (Path.implode path));
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   122
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   123
val rm = OS.FileSys.remove o platform_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 mkdir path = system_command ("mkdir -p " ^ shell_path path);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   126
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   127
fun is_dir path =
19473
wenzelm
parents: 18715
diff changeset
   128
  the_default false (try OS.FileSys.isDir (platform_path path));
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   129
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   130
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   131
(* open files *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   132
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   133
local
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   134
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   135
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
   136
  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
   137
  in Exn.release (Exn.capture f file before close_file file) end;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
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
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   145
end;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   146
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   147
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   148
(* input *)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   149
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   150
(*scalable iterator -- avoid size limit of TextIO.inputAll, and overhead of many TextIO.inputLine*)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   151
fun fold_lines f path a = open_input (fn file =>
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   152
  let
28050
7cef47b53feb fold_lines: simplified, more efficient due to String.fields;
wenzelm
parents: 28028
diff changeset
   153
    val split = split_last o String.fields (fn c => str c = "\n");
28051
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   154
    fun read buf =
28050
7cef47b53feb fold_lines: simplified, more efficient due to String.fields;
wenzelm
parents: 28028
diff changeset
   155
      (case split (TextIO.input file) of
28051
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   156
        ([], "") => (case Buffer.content buf of "" => I | line => f line)
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   157
      | ([], rest) => read (Buffer.add rest buf)
28050
7cef47b53feb fold_lines: simplified, more efficient due to String.fields;
wenzelm
parents: 28028
diff changeset
   158
      | (line :: lines, rest) =>
28051
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   159
          f (Buffer.content (Buffer.add line buf))
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   160
          #> fold f lines
56e3a695434f tuned fold_lines;
wenzelm
parents: 28050
diff changeset
   161
          #> read (Buffer.add rest Buffer.empty));
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   162
  in read Buffer.empty a end) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   163
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   164
val read = open_input TextIO.inputAll;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   165
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   166
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   167
(* output *)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   168
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   169
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
   170
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   171
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
   172
fun append_list path txts = open_append (output txts) path;
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   173
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   174
fun write path txt = write_list path [txt];
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   175
fun append path txt = append_list path [txt];
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   176
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   177
fun write_buffer path buf = open_output (Buffer.output buf) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   178
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   179
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   180
(* copy *)
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   181
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   182
fun eq paths =
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   183
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
26656
62fff5feb756 Library.is_equal;
wenzelm
parents: 26503
diff changeset
   184
    SOME ids => is_equal (OS.FileSys.compare ids)
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   185
  | NONE => false);
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   186
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   187
fun copy src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   188
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   189
  else
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   190
    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
   191
    in write target (read src) end;
6318
4a423e8a0b54 added mkdir;
wenzelm
parents: 6224
diff changeset
   192
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   193
fun copy_dir src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   194
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   195
  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
6640
d2e8342bf5c3 rearranged order of modules;
wenzelm
parents: 6318
diff changeset
   196
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   197
end;