src/Pure/Thy/file.ML

added tmp_name;

(*  Title:      Pure/Thy/file.ML
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

File system operations.
*)

signature BASIC_FILE =
sig
  val maketest: string -> unit
end;

signature FILE =
sig
  include BASIC_FILE
  val tmp_name: string -> string
  val exists: string -> bool
  val info: string -> string
  val read: string -> string
  val write: string -> string -> unit
  val append: string -> string -> unit
  val copy: string -> string -> unit
end;

structure File: FILE =
struct


(* tmp_name *)

fun tmp_name name =
  Path.pack (Path.evaluate (Path.unpack o getenv)
    (Path.append (Path.variable "ISABELLE_TMP") (Path.unpack name)));


(* exists / info *)

fun exists name = (file_info name <> "");
val info = file_info;


(* read / write files *)

fun read name =
  let
    val instream  = TextIO.openIn name;
    val intext = TextIO.inputAll instream;
  in
    TextIO.closeIn instream;
    intext
  end;

fun write name txt =
  let val outstream = TextIO.openOut name in
    TextIO.output (outstream, txt);
    TextIO.closeOut outstream
  end;

fun append name txt =
  let val outstream = TextIO.openAppend name in
    TextIO.output (outstream, txt);
    TextIO.closeOut outstream
  end;

fun copy infile outfile =
  if not (exists infile) then error ("File not found: " ^ quote infile)
  else write outfile (read infile);


(*for the "test" target in IsaMakefiles -- signifies successful termination*)
fun maketest msg =
  (writeln msg; write "test" "Test examples ran successfully\n");


end;


structure BasicFile: BASIC_FILE = File;
open BasicFile;