src/Pure/Thy/file.ML
author wenzelm
Wed, 12 Nov 1997 16:23:11 +0100
changeset 4216 419113535e48
child 4341 4adf0b093275
permissions -rw-r--r--
File system operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4216
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Thy/file.ML
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     4
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     5
File system operations.
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     6
*)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     7
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     8
signature BASIC_FILE =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
     9
sig
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    10
  val maketest: string -> unit
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    11
end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    12
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    13
signature FILE =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    14
sig
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    15
  include BASIC_FILE
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    16
  val exists: string -> bool
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    17
  val read: string -> string
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    18
  val write: string -> string -> unit
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    19
  val append: string -> string -> unit
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    20
  val copy: string -> string -> unit
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    21
end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    22
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    23
structure File: FILE =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    24
struct
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    25
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    26
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    27
(* exists *)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    28
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    29
fun exists name = (file_info name <> "");
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    30
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    31
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    32
(* read / write files *)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    33
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    34
fun read name =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    35
  let
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    36
    val instream  = TextIO.openIn name;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    37
    val intext = TextIO.inputAll instream;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    38
  in
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    39
    TextIO.closeIn instream;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    40
    intext
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    41
  end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    42
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    43
fun write name txt =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    44
  let val outstream = TextIO.openOut name in
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    45
    TextIO.output (outstream, txt);
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    46
    TextIO.closeOut outstream
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    47
  end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    48
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    49
fun append name txt =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    50
  let val outstream = TextIO.openAppend name in
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    51
    TextIO.output (outstream, txt);
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    52
    TextIO.closeOut outstream
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    53
  end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    54
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    55
fun copy infile outfile =               (* FIXME improve *)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    56
  if not (exists infile) then error ("File not found: " ^ quote infile)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    57
  else write outfile (read infile);
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    58
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    59
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    60
(*for the "test" target in IsaMakefiles -- signifies successful termination*)
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    61
fun maketest msg =
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    62
  (writeln msg; write "test" "Test examples ran successfully\n");
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    63
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    64
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    65
end;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    66
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    67
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    68
structure BasicFile: BASIC_FILE = File;
419113535e48 File system operations.
wenzelm
parents:
diff changeset
    69
open BasicFile;