src/Pure/General/file.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12116 4027b15377a5
child 12894 61f485eb0dc2
permissions -rw-r--r--
changed Thm.varifyT';
wenzelm@6118
     1
(*  Title:      Pure/General/file.ML
wenzelm@5009
     2
    ID:         $Id$
wenzelm@5009
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8806
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@5009
     5
wenzelm@5009
     6
File system operations.
wenzelm@5009
     7
*)
wenzelm@5009
     8
wenzelm@5009
     9
signature FILE =
wenzelm@5009
    10
sig
wenzelm@6224
    11
  val sys_pack_fn: (Path.T -> string) ref
wenzelm@6224
    12
  val sys_unpack_fn: (string -> Path.T) ref
wenzelm@7129
    13
  val sysify_path: Path.T -> string
wenzelm@9784
    14
  val quote_sysify_path: Path.T -> string
wenzelm@6224
    15
  val rm: Path.T -> unit
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@6182
    20
  val read: Path.T -> string
wenzelm@6182
    21
  val write: Path.T -> string -> unit
wenzelm@6182
    22
  val append: Path.T -> string -> unit
berghofe@9046
    23
  val system_command: string -> unit
wenzelm@6182
    24
  val copy: Path.T -> Path.T -> unit
wenzelm@6224
    25
  eqtype info
wenzelm@6224
    26
  val info: Path.T -> info option
wenzelm@6224
    27
  val exists: Path.T -> bool
wenzelm@6318
    28
  val mkdir: Path.T -> unit
wenzelm@7716
    29
  val copy_all: Path.T -> Path.T -> unit
wenzelm@12116
    30
  val use: Path.T -> unit
wenzelm@5009
    31
end;
wenzelm@5009
    32
wenzelm@5009
    33
structure File: FILE =
wenzelm@5009
    34
struct
wenzelm@5009
    35
wenzelm@5009
    36
wenzelm@6224
    37
(* system path representations (default: Unix) *)
wenzelm@6224
    38
wenzelm@6224
    39
val sys_pack_fn = ref Path.pack;
wenzelm@6224
    40
val sys_unpack_fn = ref Path.unpack;
wenzelm@6224
    41
wenzelm@7129
    42
fun sysify_path path = ! sys_pack_fn (Path.expand path);
wenzelm@9784
    43
val quote_sysify_path = enclose "'" "'" o sysify_path;
wenzelm@7129
    44
fun unsysify_path s = ! sys_unpack_fn s;
wenzelm@6224
    45
wenzelm@7129
    46
val rm = OS.FileSys.remove o sysify_path;
wenzelm@6224
    47
wenzelm@6224
    48
wenzelm@6224
    49
(* current path *)
wenzelm@6224
    50
wenzelm@7129
    51
val cd = Library.cd o sysify_path;
wenzelm@7129
    52
val pwd = unsysify_path o Library.pwd;
wenzelm@6224
    53
wenzelm@6224
    54
fun full_path path =
wenzelm@6224
    55
  if Path.is_absolute path then path
wenzelm@6224
    56
  else Path.append (pwd ()) path;
wenzelm@5009
    57
wenzelm@6182
    58
wenzelm@6182
    59
(* tmp_path *)
wenzelm@6182
    60
wenzelm@6182
    61
fun tmp_path path =
wenzelm@6182
    62
  Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
wenzelm@5009
    63
wenzelm@5009
    64
wenzelm@6224
    65
(* read / write files *)
wenzelm@6224
    66
wenzelm@6224
    67
fun fail_safe f g x =
wenzelm@6224
    68
  let val y = f x handle exn => (g x; raise exn)
wenzelm@6224
    69
  in g x; y end;
wenzelm@6224
    70
wenzelm@6224
    71
wenzelm@6224
    72
fun output txt stream = TextIO.output (stream, txt);
wenzelm@6182
    73
wenzelm@7129
    74
fun read path = fail_safe TextIO.inputAll TextIO.closeIn (TextIO.openIn (sysify_path path));
wenzelm@7129
    75
fun write path txt = fail_safe (output txt) TextIO.closeOut (TextIO.openOut (sysify_path path));
wenzelm@7716
    76
fun append path txt =
wenzelm@7716
    77
  fail_safe (output txt) TextIO.closeOut (TextIO.openAppend (sysify_path path));
wenzelm@6218
    78
wenzelm@6224
    79
fun copy inpath outpath = write outpath (read inpath);
wenzelm@6224
    80
wenzelm@6224
    81
wenzelm@6224
    82
(* file info *)
wenzelm@6224
    83
wenzelm@6224
    84
datatype info = Info of string;
wenzelm@5009
    85
wenzelm@6182
    86
fun info path =
wenzelm@7129
    87
  let val name = sysify_path path in
wenzelm@6182
    88
    (case file_info name of
wenzelm@6182
    89
      "" => None
wenzelm@6224
    90
    | s => Some (Info s))
wenzelm@6182
    91
  end;
wenzelm@6182
    92
wenzelm@6182
    93
val exists = is_some o info;
wenzelm@5009
    94
wenzelm@5009
    95
wenzelm@7716
    96
(* directories *)
wenzelm@6318
    97
wenzelm@7850
    98
fun system_command cmd =
wenzelm@7850
    99
  if system cmd <> 0 then error ("System command failed: " ^ cmd)
wenzelm@7850
   100
  else ();
wenzelm@7850
   101
    
wenzelm@9784
   102
fun mkdir path = system_command ("mkdir -p " ^ quote_sysify_path path);
wenzelm@6640
   103
wenzelm@8163
   104
fun copy_all path1 path2 =  (*dereferences symlinks!*)
wenzelm@9784
   105
  system_command ("cp -r " ^ quote_sysify_path path1 ^ " " ^ quote_sysify_path path2);
wenzelm@6640
   106
wenzelm@6640
   107
wenzelm@12116
   108
(* use ML files *)
wenzelm@6640
   109
wenzelm@12116
   110
val use = use o sysify_path;
wenzelm@6640
   111
wenzelm@5009
   112
end;