# HG changeset patch
# User wenzelm
# Date 870869390 -7200
# Node ID 36e19fce289ea79c5843390440b0636c3bb084bf
# Parent  e843c1d6f9e1a93a699e7e3f32ba69521f954046
added read_file, write_file;

diff -r e843c1d6f9e1 -r 36e19fce289e src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Aug 06 11:58:50 1997 +0200
+++ b/src/Pure/library.ML	Wed Aug 06 14:09:50 1997 +0200
@@ -770,13 +770,30 @@
                         else error (msg_fn x)
   in  asl l  end;
 
-(*for the "test" target in Makefiles -- signifies successful termination*)
+
+(* read / write files *)
+
+fun read_file name =
+  let
+    val instream  = TextIO.openIn name;
+    val intext = TextIO.inputAll instream;
+  in
+    TextIO.closeIn instream;
+    intext
+  end;
+
+fun write_file name txt =
+  let
+    val outstream = TextIO.openOut name;
+  in
+    TextIO.output (outstream, txt);
+    TextIO.closeOut outstream
+  end;
+
+
+(*for the "test" target in IsaMakefiles -- signifies successful termination*)
 fun maketest msg =
-  (writeln msg; 
-   let val os = TextIO.openOut "test" 
-   in  TextIO.output (os, "Test examples ran successfully\n");
-       TextIO.closeOut os
-   end);
+  (writeln msg; write_file "test" "Test examples ran successfully\n");
 
 
 (*print a list surrounded by the brackets lpar and rpar, with comma separator
@@ -816,7 +833,7 @@
   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
    writeln ("\n**** Finished " ^ fname ^ " ****")));
 
-(*For Makefiles: use the file, but exit with error code if errors found.*)
+(*use the file, but exit with error code if errors found.*)
 fun exit_use fname = use fname handle _ => exit 1;