src/Pure/General/file.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23861 72bb3494746f
child 23874 4642a2eefe74
permissions -rw-r--r--
tuned signature;
wenzelm@6118
     1
(*  Title:      Pure/General/file.ML
wenzelm@5009
     2
    ID:         $Id$
wenzelm@5009
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5009
     4
wenzelm@5009
     5
File system operations.
wenzelm@5009
     6
*)
wenzelm@5009
     7
wenzelm@5009
     8
signature FILE =
wenzelm@5009
     9
sig
wenzelm@21858
    10
  val explode_platform_path_fn: (string -> Path.T) ref
wenzelm@21858
    11
  val explode_platform_path: string -> Path.T
wenzelm@16261
    12
  val platform_path_fn: (Path.T -> string) ref
wenzelm@16261
    13
  val platform_path: Path.T -> string
wenzelm@16261
    14
  val shell_path_fn: (Path.T -> string) ref
wenzelm@16261
    15
  val shell_path: Path.T -> string
wenzelm@6224
    16
  val cd: Path.T -> unit
wenzelm@6224
    17
  val pwd: unit -> Path.T
wenzelm@6224
    18
  val full_path: Path.T -> Path.T
wenzelm@6182
    19
  val tmp_path: Path.T -> Path.T
wenzelm@16261
    20
  val isatool: string -> int
wenzelm@16261
    21
  val system_command: string -> unit
wenzelm@23861
    22
  eqtype ident
wenzelm@23861
    23
  val ident: Path.T -> ident option
wenzelm@17826
    24
  val exists: Path.T -> bool
wenzelm@21858
    25
  val check: Path.T -> unit
wenzelm@17826
    26
  val rm: Path.T -> unit
wenzelm@17826
    27
  val mkdir: Path.T -> unit
wenzelm@6182
    28
  val read: Path.T -> string
wenzelm@6182
    29
  val write: Path.T -> string -> unit
wenzelm@6182
    30
  val append: Path.T -> string -> unit
wenzelm@16713
    31
  val write_list: Path.T -> string list -> unit
wenzelm@16713
    32
  val append_list: Path.T -> string list -> unit
wenzelm@16603
    33
  val eq: Path.T * Path.T -> bool
wenzelm@6182
    34
  val copy: Path.T -> Path.T -> unit
wenzelm@16261
    35
  val copy_dir: Path.T -> Path.T -> unit
wenzelm@5009
    36
end;
wenzelm@5009
    37
wenzelm@5009
    38
structure File: FILE =
wenzelm@5009
    39
struct
wenzelm@5009
    40
wenzelm@16261
    41
(* platform specific path representations *)
wenzelm@6224
    42
wenzelm@21858
    43
val explode_platform_path_fn = ref Path.explode;
wenzelm@21858
    44
fun explode_platform_path s = ! explode_platform_path_fn s;
wenzelm@6224
    45
wenzelm@21858
    46
val platform_path_fn = ref (Path.implode o Path.expand);
wenzelm@16261
    47
fun platform_path path = ! platform_path_fn path;
wenzelm@6224
    48
wenzelm@21858
    49
val shell_path_fn = ref (enclose "'" "'" o Path.implode o Path.expand);
wenzelm@16261
    50
fun shell_path path = ! shell_path_fn path;
wenzelm@6224
    51
wenzelm@6224
    52
wenzelm@6224
    53
(* current path *)
wenzelm@6224
    54
wenzelm@23826
    55
val cd = cd o platform_path;
wenzelm@23826
    56
val pwd = explode_platform_path o pwd;
wenzelm@6224
    57
berghofe@15155
    58
fun norm_absolute p =
berghofe@15155
    59
  let
berghofe@15155
    60
    val p' = pwd ();
berghofe@15155
    61
    fun norm p = if can cd p then pwd ()
berghofe@15155
    62
      else Path.append (norm (Path.dir p)) (Path.base p);
wenzelm@16261
    63
    val p'' = norm p;
berghofe@15155
    64
  in (cd p'; p'') end
berghofe@15155
    65
wenzelm@16261
    66
fun full_path path =
berghofe@15155
    67
  (if Path.is_absolute path then path
wenzelm@16261
    68
   else Path.append (pwd ()) path)
wenzelm@16261
    69
  |> norm_absolute;
wenzelm@5009
    70
wenzelm@6182
    71
wenzelm@6182
    72
(* tmp_path *)
wenzelm@6182
    73
wenzelm@6182
    74
fun tmp_path path =
wenzelm@6182
    75
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
wenzelm@5009
    76
wenzelm@5009
    77
wenzelm@16261
    78
(* system commands *)
wenzelm@16261
    79
wenzelm@16261
    80
fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
wenzelm@16261
    81
wenzelm@16261
    82
fun system_command cmd =
wenzelm@16261
    83
  if system cmd <> 0 then error ("System command failed: " ^ cmd)
wenzelm@16261
    84
  else ();
wenzelm@16261
    85
wenzelm@16261
    86
wenzelm@16261
    87
(* directory entries *)
wenzelm@16261
    88
wenzelm@23861
    89
datatype ident = Ident of string;
wenzelm@16261
    90
wenzelm@23861
    91
fun ident path =
wenzelm@23861
    92
  (case try OS.FileSys.modTime (platform_path path) of
wenzelm@23861
    93
    NONE => NONE
wenzelm@23861
    94
  | SOME time => SOME (Ident
wenzelm@23861
    95
      (case getenv "ISABELLE_FILE_IDENT" of
wenzelm@23861
    96
        "" => Path.implode (full_path path) ^ ": " ^ Time.toString time
wenzelm@23861
    97
      | cmd =>
wenzelm@23861
    98
         let val id = execute ("\"$ISABELLE_HOME/lib/scripts/fileident\" " ^ shell_path path) in
wenzelm@23861
    99
           if id <> "" then id
wenzelm@23861
   100
           else error ("Failed to identify file " ^ quote (Path.implode path) ^ " by " ^ cmd)
wenzelm@23861
   101
         end)));
wenzelm@16261
   102
wenzelm@23861
   103
val exists = can OS.FileSys.modTime o platform_path;
wenzelm@16261
   104
wenzelm@21858
   105
fun check path =
wenzelm@17826
   106
  if exists path then ()
wenzelm@21858
   107
  else error ("No such file or directory: " ^ quote (Path.implode path));
wenzelm@17826
   108
wenzelm@16261
   109
val rm = OS.FileSys.remove o platform_path;
wenzelm@16261
   110
wenzelm@16261
   111
fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
wenzelm@16261
   112
wenzelm@16261
   113
fun is_dir path =
wenzelm@19473
   114
  the_default false (try OS.FileSys.isDir (platform_path path));
wenzelm@16261
   115
wenzelm@16261
   116
wenzelm@6224
   117
(* read / write files *)
wenzelm@6224
   118
wenzelm@16261
   119
local
wenzelm@16261
   120
wenzelm@6224
   121
fun fail_safe f g x =
wenzelm@6224
   122
  let val y = f x handle exn => (g x; raise exn)
wenzelm@6224
   123
  in g x; y end;
wenzelm@6224
   124
wenzelm@16713
   125
fun output txts stream = List.app (fn txt => TextIO.output (stream, txt)) txts;
wenzelm@6182
   126
wenzelm@16261
   127
in
wenzelm@6218
   128
wenzelm@16261
   129
fun read path =
wenzelm@16261
   130
  fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (platform_path path));
wenzelm@6224
   131
wenzelm@16713
   132
fun write_list path txts =
wenzelm@16713
   133
  fail_safe (output txts) TextIO.closeOut (TextIO.openOut (platform_path path));
wenzelm@5009
   134
wenzelm@16713
   135
fun append_list path txts =
wenzelm@16713
   136
  fail_safe (output txts) TextIO.closeOut (TextIO.openAppend (platform_path path));
wenzelm@16713
   137
wenzelm@16713
   138
fun write path txt = write_list path [txt];
wenzelm@16713
   139
fun append path txt = append_list path [txt];
wenzelm@6182
   140
wenzelm@16261
   141
end;
wenzelm@5009
   142
wenzelm@16603
   143
fun eq paths =
wenzelm@16603
   144
  (case try (pairself (OS.FileSys.fileId o platform_path)) paths of
wenzelm@16603
   145
    SOME ids => OS.FileSys.compare ids = EQUAL
wenzelm@16603
   146
  | NONE => false);
wenzelm@16603
   147
wenzelm@21962
   148
fun copy src dst =
wenzelm@21962
   149
  if eq (src, dst) then ()
wenzelm@21962
   150
  else
wenzelm@21962
   151
    let val target = if is_dir dst then Path.append dst (Path.base src) else dst
wenzelm@21962
   152
    in write target (read src) end;
wenzelm@6318
   153
wenzelm@21962
   154
fun copy_dir src dst =
wenzelm@21962
   155
  if eq (src, dst) then ()
wenzelm@21962
   156
  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
wenzelm@6640
   157
wenzelm@5009
   158
end;