src/Pure/General/file.ML
author wenzelm
Thu, 06 Mar 2008 20:17:50 +0100
changeset 26220 d34b68c21f9a
parent 24446 bb7a85ea57cf
child 26503 4dec4460244f
permissions -rw-r--r--
common setup for system_out/system;
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
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    10
  val explode_platform_path_fn: (string -> Path.T) ref
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    11
  val explode_platform_path: string -> Path.T
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    12
  val platform_path_fn: (Path.T -> string) ref
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    13
  val platform_path: Path.T -> string
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    14
  val shell_path_fn: (Path.T -> string) ref
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    15
  val shell_path: Path.T -> string
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    16
  val cd: Path.T -> unit
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    17
  val pwd: unit -> Path.T
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    18
  val full_path: Path.T -> Path.T
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    19
  val tmp_path: Path.T -> Path.T
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    20
  val isatool: string -> int
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    21
  val system_command: string -> unit
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    22
  eqtype ident
23874
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    23
  val rep_ident: ident -> string
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    24
  val ident: Path.T -> ident option
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    25
  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
    26
  val check: Path.T -> unit
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    27
  val rm: Path.T -> unit
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
    28
  val mkdir: Path.T -> unit
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
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
    34
  val eq: Path.T * Path.T -> bool
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    35
  val copy: Path.T -> Path.T -> unit
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    36
  val copy_dir: Path.T -> Path.T -> unit
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    37
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    38
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    39
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    40
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    41
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    42
(* platform specific path representations *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    43
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    44
val explode_platform_path_fn = ref Path.explode;
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    45
fun explode_platform_path s = ! explode_platform_path_fn s;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    46
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    47
val platform_path_fn = ref (Path.implode o Path.expand);
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    48
fun platform_path path = ! platform_path_fn path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    49
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
    50
val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    51
fun shell_path path = ! shell_path_fn path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    52
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    53
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    54
(* current path *)
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    55
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    56
val cd = cd o platform_path;
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    57
val pwd = explode_platform_path o pwd;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    58
24446
bb7a85ea57cf norm_absolute: CRITICAL;
wenzelm
parents: 24360
diff changeset
    59
fun norm_absolute p = NAMED_CRITICAL "IO" (fn () =>
15155
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    60
  let
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    61
    val p' = pwd ();
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    62
    fun norm p = if can cd p then pwd ()
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    63
      else Path.append (norm (Path.dir p)) (Path.base p);
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    64
    val p'' = norm p;
24446
bb7a85ea57cf norm_absolute: CRITICAL;
wenzelm
parents: 24360
diff changeset
    65
  in (cd p'; p'') end);
15155
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    66
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    67
fun full_path path =
15155
6cdd6a8da9b9 Added function for "normalizing" absolute paths (i.e. dereferencing of
berghofe
parents: 14981
diff changeset
    68
  (if Path.is_absolute path then path
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    69
   else Path.append (pwd ()) path)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    70
  |> norm_absolute;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    71
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    72
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    73
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    74
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    75
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    76
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    77
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    78
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    79
(* system commands *)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    80
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    81
fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    82
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    83
fun system_command cmd =
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    84
  if system cmd <> 0 then error ("System command failed: " ^ cmd)
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    85
  else ();
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    86
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    87
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    88
(* directory entries *)
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;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    91
23874
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    92
fun rep_ident (Ident s) = s;
4642a2eefe74 added rep_ident;
wenzelm
parents: 23861
diff changeset
    93
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    94
fun ident path =
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    95
  (case try OS.FileSys.modTime (platform_path path) of
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    96
    NONE => NONE
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    97
  | SOME time => SOME (Ident
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    98
      (case getenv "ISABELLE_FILE_IDENT" of
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    99
        "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   100
      | cmd =>
26220
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 24446
diff changeset
   101
         let
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 24446
diff changeset
   102
           val (id, rc) = system_out ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path)
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 24446
diff changeset
   103
         in
d34b68c21f9a common setup for system_out/system;
wenzelm
parents: 24446
diff changeset
   104
           if id <> "" andalso rc = 0 then id
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   105
           else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   106
         end)));
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   107
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
   108
val exists = can OS.FileSys.modTime o platform_path;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   109
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 19960
diff changeset
   110
fun check path =
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   111
  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
   112
  else error ("No such file or directory: " ^ quote (Path.implode path));
17826
afa2696eacce added assert;
wenzelm
parents: 16713
diff changeset
   113
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   114
val rm = OS.FileSys.remove o platform_path;
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   115
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   116
fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   117
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   118
fun is_dir path =
19473
wenzelm
parents: 18715
diff changeset
   119
  the_default false (try OS.FileSys.isDir (platform_path path));
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   120
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   121
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   122
(* read / write files *)
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   123
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   124
local
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   125
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   126
fun fail_safe f g x =
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   127
  let val y = f x handle exn => (g x; raise exn)
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   128
  in g x; y end;
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   129
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   130
fun output txts stream = List.app (fn txt => TextIO.output (stream, txt)) txts;
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   131
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   132
in
6218
3e9d6edc99a8 added join_info;
wenzelm
parents: 6182
diff changeset
   133
24360
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   134
fun read path =
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   135
  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   136
24360
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   137
fun write_list path txts =
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   138
  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   139
24360
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   140
fun append_list path txts =
a0da34cc081c File.read/write/append: non-critical (basic IO operations already thread-safe);
wenzelm
parents: 24058
diff changeset
   141
  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   142
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   143
fun write path txt = write_list path [txt];
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   144
fun append path txt = append_list path [txt];
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   145
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   146
end;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   147
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   148
fun eq paths =
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   149
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   150
    SOME ids => OS.FileSys.compare ids = EQUAL
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   151
  | NONE => false);
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   152
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   153
fun copy src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   154
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   155
  else
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   156
    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
   157
    in write target (read src) end;
6318
4a423e8a0b54 added mkdir;
wenzelm
parents: 6224
diff changeset
   158
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   159
fun copy_dir src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   160
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   161
  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
6640
d2e8342bf5c3 rearranged order of modules;
wenzelm
parents: 6318
diff changeset
   162
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   163
end;