src/Pure/General/file.ML
author wenzelm
Thu Aug 23 17:46:03 2012 +0200 (2012-08-23)
changeset 48911 5debc3e4fa81
parent 48446 8f611bc3650b
child 56533 cd8b6d849b6a
permissions -rw-r--r--
tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm@6118
     1
(*  Title:      Pure/General/file.ML
wenzelm@5009
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5009
     3
wenzelm@5009
     4
File system operations.
wenzelm@5009
     5
*)
wenzelm@5009
     6
wenzelm@5009
     7
signature FILE =
wenzelm@5009
     8
sig
wenzelm@16261
     9
  val platform_path: Path.T -> string
wenzelm@32943
    10
  val shell_quote: string -> string
wenzelm@16261
    11
  val shell_path: Path.T -> string
wenzelm@6224
    12
  val cd: Path.T -> unit
wenzelm@6224
    13
  val pwd: unit -> Path.T
wenzelm@42003
    14
  val full_path: Path.T -> Path.T -> Path.T
wenzelm@6182
    15
  val tmp_path: Path.T -> Path.T
wenzelm@17826
    16
  val exists: Path.T -> bool
wenzelm@17826
    17
  val rm: Path.T -> unit
wenzelm@40785
    18
  val is_dir: Path.T -> bool
wenzelm@42003
    19
  val check_dir: Path.T -> Path.T
wenzelm@42003
    20
  val check_file: Path.T -> Path.T
wenzelm@43848
    21
  val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
wenzelm@26503
    22
  val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
wenzelm@26503
    23
  val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
wenzelm@26503
    24
  val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
wenzelm@43848
    25
  val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
wenzelm@43848
    26
  val read_dir: Path.T -> string list
wenzelm@28028
    27
  val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
wenzelm@43845
    28
  val fold_pages: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
wenzelm@43848
    29
  val read_lines: Path.T -> string list
wenzelm@44879
    30
  val read_pages: Path.T -> string list
wenzelm@6182
    31
  val read: Path.T -> string
wenzelm@6182
    32
  val write: Path.T -> string -> unit
wenzelm@6182
    33
  val append: Path.T -> string -> unit
wenzelm@16713
    34
  val write_list: Path.T -> string list -> unit
wenzelm@16713
    35
  val append_list: Path.T -> string list -> unit
wenzelm@28028
    36
  val write_buffer: Path.T -> Buffer.T -> unit
wenzelm@16603
    37
  val eq: Path.T * Path.T -> bool
wenzelm@6182
    38
  val copy: Path.T -> Path.T -> unit
wenzelm@5009
    39
end;
wenzelm@5009
    40
wenzelm@5009
    41
structure File: FILE =
wenzelm@5009
    42
struct
wenzelm@5009
    43
wenzelm@26503
    44
(* system path representations *)
wenzelm@6224
    45
wenzelm@26503
    46
val platform_path = Path.implode o Path.expand;
wenzelm@26980
    47
wenzelm@48446
    48
val shell_quote = enclose "'" "'";
wenzelm@26980
    49
val shell_path = shell_quote o platform_path;
wenzelm@6224
    50
wenzelm@6224
    51
wenzelm@26503
    52
(* current working directory *)
wenzelm@6224
    53
wenzelm@23826
    54
val cd = cd o platform_path;
wenzelm@26503
    55
val pwd = Path.explode o pwd;
wenzelm@6224
    56
wenzelm@42003
    57
wenzelm@42003
    58
(* full_path *)
wenzelm@42003
    59
wenzelm@42003
    60
fun full_path dir path =
wenzelm@42003
    61
  let
wenzelm@42003
    62
    val path' = Path.expand path;
wenzelm@42003
    63
    val _ = Path.is_current path' andalso error "Bad file specification";
wenzelm@42003
    64
    val path'' = Path.append dir path';
wenzelm@42003
    65
  in
wenzelm@42003
    66
    if Path.is_absolute path'' then path''
wenzelm@42003
    67
    else Path.append (pwd ()) path''
wenzelm@42003
    68
  end;
wenzelm@5009
    69
wenzelm@6182
    70
wenzelm@6182
    71
(* tmp_path *)
wenzelm@6182
    72
wenzelm@6182
    73
fun tmp_path path =
wenzelm@6182
    74
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
wenzelm@5009
    75
wenzelm@5009
    76
wenzelm@26980
    77
(* directory entries *)
wenzelm@26980
    78
wenzelm@23861
    79
val exists = can OS.FileSys.modTime o platform_path;
wenzelm@16261
    80
wenzelm@16261
    81
val rm = OS.FileSys.remove o platform_path;
wenzelm@16261
    82
wenzelm@40785
    83
fun is_dir path =
wenzelm@40785
    84
  the_default false (try OS.FileSys.isDir (platform_path path));
wenzelm@40785
    85
wenzelm@42003
    86
fun check_dir path =
wenzelm@42003
    87
  if exists path andalso is_dir path then path
wenzelm@42003
    88
  else error ("No such directory: " ^ Path.print path);
wenzelm@42003
    89
wenzelm@42003
    90
fun check_file path =
wenzelm@42003
    91
  if exists path andalso not (is_dir path) then path
wenzelm@42003
    92
  else error ("No such file: " ^ Path.print path);
wenzelm@42003
    93
wenzelm@16261
    94
wenzelm@43848
    95
(* open streams *)
wenzelm@6224
    96
wenzelm@16261
    97
local
wenzelm@16261
    98
wenzelm@26503
    99
fun with_file open_file close_file f path =
wenzelm@26503
   100
  let val file = open_file path
wenzelm@26503
   101
  in Exn.release (Exn.capture f file before close_file file) end;
wenzelm@6224
   102
wenzelm@16261
   103
in
wenzelm@6218
   104
wenzelm@43848
   105
fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
wenzelm@26503
   106
fun open_input f = with_file TextIO.openIn TextIO.closeIn f o platform_path;
wenzelm@26503
   107
fun open_output f = with_file TextIO.openOut TextIO.closeOut f o platform_path;
wenzelm@26503
   108
fun open_append f = with_file TextIO.openAppend TextIO.closeOut f o platform_path;
wenzelm@6224
   109
wenzelm@28028
   110
end;
wenzelm@28028
   111
wenzelm@28028
   112
wenzelm@43848
   113
(* directory content *)
wenzelm@43848
   114
wenzelm@43848
   115
fun fold_dir f path a = open_dir (fn stream =>
wenzelm@43848
   116
  let
wenzelm@43848
   117
    fun read x =
wenzelm@43848
   118
      (case OS.FileSys.readDir stream of
wenzelm@43848
   119
        NONE => x
wenzelm@43848
   120
      | SOME entry => read (f entry x));
wenzelm@43848
   121
  in read a end) path;
wenzelm@43848
   122
wenzelm@43848
   123
fun read_dir path = rev (fold_dir cons path []);
wenzelm@43848
   124
wenzelm@43848
   125
wenzelm@28028
   126
(* input *)
wenzelm@28028
   127
wenzelm@44879
   128
(*
wenzelm@44879
   129
  scalable iterator:
wenzelm@44879
   130
  . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
wenzelm@48911
   131
  . optional terminator at end-of-input
wenzelm@44879
   132
*)
wenzelm@43845
   133
fun fold_chunks terminator f path a = open_input (fn file =>
wenzelm@28028
   134
  let
wenzelm@28510
   135
    fun read buf x =
wenzelm@28510
   136
      (case TextIO.input file of
wenzelm@28510
   137
        "" => (case Buffer.content buf of "" => x | line => f line x)
wenzelm@28510
   138
      | input =>
wenzelm@43845
   139
          (case String.fields (fn c => c = terminator) input of
wenzelm@28510
   140
            [rest] => read (Buffer.add rest buf) x
noschinl@43616
   141
          | line :: more => read_lines more (f (Buffer.content (Buffer.add line buf)) x)))
noschinl@43616
   142
    and read_lines [rest] x = read (Buffer.add rest Buffer.empty) x
noschinl@43616
   143
      | read_lines (line :: more) x = read_lines more (f line x);
wenzelm@28028
   144
  in read Buffer.empty a end) path;
wenzelm@28028
   145
wenzelm@43845
   146
fun fold_lines f = fold_chunks #"\n" f;
wenzelm@43845
   147
fun fold_pages f = fold_chunks #"\f" f;
wenzelm@43845
   148
wenzelm@43848
   149
fun read_lines path = rev (fold_lines cons path []);
wenzelm@44879
   150
fun read_pages path = rev (fold_pages cons path []);
wenzelm@43848
   151
wenzelm@26503
   152
val read = open_input TextIO.inputAll;
wenzelm@5009
   153
wenzelm@28028
   154
wenzelm@28028
   155
(* output *)
wenzelm@28028
   156
wenzelm@28028
   157
fun output txts file = List.app (fn txt => TextIO.output (file, txt)) txts;
wenzelm@28028
   158
wenzelm@26503
   159
fun write_list path txts = open_output (output txts) path;
wenzelm@26503
   160
fun append_list path txts = open_append (output txts) path;
wenzelm@16713
   161
wenzelm@16713
   162
fun write path txt = write_list path [txt];
wenzelm@16713
   163
fun append path txt = append_list path [txt];
wenzelm@6182
   164
wenzelm@28028
   165
fun write_buffer path buf = open_output (Buffer.output buf) path;
wenzelm@28028
   166
wenzelm@28028
   167
wenzelm@28028
   168
(* copy *)
wenzelm@5009
   169
wenzelm@16603
   170
fun eq paths =
wenzelm@16603
   171
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
wenzelm@26656
   172
    SOME ids => is_equal (OS.FileSys.compare ids)
wenzelm@16603
   173
  | NONE => false);
wenzelm@16603
   174
wenzelm@21962
   175
fun copy src dst =
wenzelm@21962
   176
  if eq (src, dst) then ()
wenzelm@21962
   177
  else
wenzelm@21962
   178
    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
wenzelm@21962
   179
    in write target (read src) end;
wenzelm@6318
   180
wenzelm@5009
   181
end;