# HG changeset patch
# User wenzelm
# Date 879348191 -3600
# Node ID 419113535e489ee03aa1c80504be4be08cddd9c0
# Parent  7f7519759b8cf378dd344e2dffd6ca70d2b38edd
File system operations.

diff -r 7f7519759b8c -r 419113535e48 src/Pure/Thy/file.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/file.ML	Wed Nov 12 16:23:11 1997 +0100
@@ -0,0 +1,69 @@
+(*  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 exists: string -> bool
+  val read: string -> string
+  val write: string -> string -> unit
+  val append: string -> string -> unit
+  val copy: string -> string -> unit
+end;
+
+structure File: FILE =
+struct
+
+
+(* exists *)
+
+fun exists name = (file_info name <> "");
+
+
+(* 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 =               (* FIXME improve *)
+  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;