src/Pure/General/file.ML
author wenzelm
Sun, 20 Mar 2011 17:40:45 +0100
changeset 42003 6e45dc518ebb
parent 41944 b97091ae583a
child 42329 782991e4180d
permissions -rw-r--r--
replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;
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
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    21
  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
    22
  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
    23
  val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    24
  val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    25
  val read: Path.T -> string
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    26
  val write: Path.T -> string -> unit
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    27
  val append: Path.T -> string -> unit
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    28
  val write_list: Path.T -> string list -> unit
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
    29
  val append_list: Path.T -> string list -> unit
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    30
  val write_buffer: Path.T -> Buffer.T -> unit
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
    31
  val eq: Path.T * Path.T -> bool
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    32
  val copy: Path.T -> Path.T -> unit
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    33
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    34
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    35
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    36
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    37
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    38
(* system path representations *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    39
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    40
val platform_path = Path.implode o Path.expand;
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    41
40746
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    42
fun shell_quote s =
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    43
  if exists_string (fn c => c = "'") s then
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    44
    error ("Illegal single quote in path specification: " ^ quote s)
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    45
  else enclose "'" "'" s;
f57ca096d8c9 explicit check for requirement;
wenzelm
parents: 40744
diff changeset
    46
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    47
val shell_path = shell_quote o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    48
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    49
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    50
(* current working directory *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    51
23826
463903573934 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
wenzelm
parents: 22145
diff changeset
    52
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
    53
val pwd = Path.explode o pwd;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    54
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    55
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    56
(* full_path *)
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    57
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    58
fun full_path dir path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    59
  let
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    60
    val path' = Path.expand path;
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    61
    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
    62
    val path'' = Path.append dir path';
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    63
  in
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    64
    if Path.is_absolute path'' then path''
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    65
    else Path.append (pwd ()) path''
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    66
  end;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    67
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    68
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    69
(* tmp_path *)
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    70
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    71
fun tmp_path path =
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
    72
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    73
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    74
26980
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    75
(* directory entries *)
f7f48bb9a025 ident: naive caching prevents potentially slow external invocations;
wenzelm
parents: 26946
diff changeset
    76
23861
72bb3494746f replaced info by ident (for full identification, potentially content-based);
wenzelm
parents: 23826
diff changeset
    77
val exists = can OS.FileSys.modTime o platform_path;
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    78
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    79
val rm = OS.FileSys.remove o platform_path;
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    80
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    81
fun is_dir path =
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    82
  the_default false (try OS.FileSys.isDir (platform_path path));
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40746
diff changeset
    83
42003
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    84
fun check_dir path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    85
  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
    86
  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
    87
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    88
fun check_file path =
6e45dc518ebb replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents: 41944
diff changeset
    89
  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
    90
  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
    91
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    92
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
    93
(* open files *)
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
    94
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    95
local
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
    96
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
    97
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
    98
  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
    99
  in Exn.release (Exn.capture f file before close_file file) end;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   100
16261
28803c418b59 removed sysify_path, quote_sysity_path etc.;
wenzelm
parents: 16002
diff changeset
   101
in
6218
3e9d6edc99a8 added join_info;
wenzelm
parents: 6182
diff changeset
   102
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   103
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
   104
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
   105
fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
6224
0c08846be6f3 fail_safe close;
wenzelm
parents: 6218
diff changeset
   106
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   107
end;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   108
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   109
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   110
(* input *)
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   111
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   112
(*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
   113
fun fold_lines f path a = open_input (fn file =>
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   114
  let
28510
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   115
    fun read buf x =
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   116
      (case TextIO.input file of
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   117
        "" => (case Buffer.content buf of "" => x | line => f line x)
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   118
      | input =>
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   119
          (case String.fields (fn c => c = #"\n") input of
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   120
            [rest] => read (Buffer.add rest buf) x
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   121
          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   122
    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
66b95e857bde fold_lines: more tuning, avoiding extra split_last;
wenzelm
parents: 28500
diff changeset
   123
      | 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
   124
  in read Buffer.empty a end) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   125
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   126
val read = open_input TextIO.inputAll;
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   127
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   128
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   129
(* output *)
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
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
   132
26503
4dec4460244f discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn;
wenzelm
parents: 26220
diff changeset
   133
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
   134
fun append_list path txts = open_append (output txts) path;
16713
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   135
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   136
fun write path txt = write_list path [txt];
be5763901788 added write_list, append_list;
wenzelm
parents: 16603
diff changeset
   137
fun append path txt = append_list path [txt];
6182
4a07dfe3583f use Path.T;
wenzelm
parents: 6118
diff changeset
   138
28028
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   139
fun write_buffer path buf = open_output (Buffer.output buf) path;
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   140
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   141
c0f54a32491e renamed Buffer.write to File.write_buffer;
wenzelm
parents: 26980
diff changeset
   142
(* copy *)
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   143
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   144
fun eq paths =
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   145
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
26656
62fff5feb756 Library.is_equal;
wenzelm
parents: 26503
diff changeset
   146
    SOME ids => is_equal (OS.FileSys.compare ids)
16603
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   147
  | NONE => false);
1776d276f848 added eq;
wenzelm
parents: 16304
diff changeset
   148
21962
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   149
fun copy src dst =
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   150
  if eq (src, dst) then ()
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   151
  else
279b129498b6 removed conditional combinator;
wenzelm
parents: 21858
diff changeset
   152
    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
   153
    in write target (read src) end;
6318
4a423e8a0b54 added mkdir;
wenzelm
parents: 6224
diff changeset
   154
5009
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
   155
end;