src/Pure/General/file.ML
author wenzelm
Wed, 13 Jan 1999 15:18:02 +0100
changeset 6118 caa439435666
parent 5009 05b152a41922
child 6182 4a07dfe3583f
permissions -rw-r--r--
fixed titles;
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
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    10
  val tmp_name: string -> string
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    11
  val exists: string -> bool
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    12
  val info: string -> string
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    13
  val read: string -> string
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    14
  val write: string -> string -> unit
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    15
  val append: string -> string -> unit
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    16
  val copy: string -> string -> unit
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    17
end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    18
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    19
structure File: FILE =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    20
struct
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    21
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    22
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    23
(* tmp_name *)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    24
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    25
fun tmp_name name =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    26
  Path.pack (Path.evaluate (Path.unpack o getenv)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    27
    (Path.append (Path.variable "ISABELLE_TMP") (Path.unpack name)));
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    28
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    29
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    30
(* exists / info *)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    31
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    32
fun exists name = (file_info name <> "");
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    33
val info = file_info;
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
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    36
(* read / write files *)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    37
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    38
fun read name =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    39
  let
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    40
    val instream  = TextIO.openIn name;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    41
    val intext = TextIO.inputAll instream;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    42
  in
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    43
    TextIO.closeIn instream;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    44
    intext
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    45
  end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    46
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    47
fun write name txt =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    48
  let val outstream = TextIO.openOut name in
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    49
    TextIO.output (outstream, txt);
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    50
    TextIO.closeOut outstream
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    51
  end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    52
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    53
fun append name txt =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    54
  let val outstream = TextIO.openAppend name in
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    55
    TextIO.output (outstream, txt);
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    56
    TextIO.closeOut outstream
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    57
  end;
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    58
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    59
fun copy infile outfile =
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    60
  if not (exists infile) then error ("File not found: " ^ quote infile)
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    61
  else write outfile (read infile);
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    62
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    63
05b152a41922 moved Thy/file.ML to General/file.ML;
wenzelm
parents:
diff changeset
    64
end;