added read_file, write_file;
authorwenzelm
Wed Aug 06 14:09:50 1997 +0200 (1997-08-06)
changeset 362436e19fce289e
parent 3623 e843c1d6f9e1
child 3625 33f718b4f7bf
added read_file, write_file;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Aug 06 11:58:50 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Aug 06 14:09:50 1997 +0200
     1.3 @@ -770,13 +770,30 @@
     1.4                          else error (msg_fn x)
     1.5    in  asl l  end;
     1.6  
     1.7 -(*for the "test" target in Makefiles -- signifies successful termination*)
     1.8 +
     1.9 +(* read / write files *)
    1.10 +
    1.11 +fun read_file name =
    1.12 +  let
    1.13 +    val instream  = TextIO.openIn name;
    1.14 +    val intext = TextIO.inputAll instream;
    1.15 +  in
    1.16 +    TextIO.closeIn instream;
    1.17 +    intext
    1.18 +  end;
    1.19 +
    1.20 +fun write_file name txt =
    1.21 +  let
    1.22 +    val outstream = TextIO.openOut name;
    1.23 +  in
    1.24 +    TextIO.output (outstream, txt);
    1.25 +    TextIO.closeOut outstream
    1.26 +  end;
    1.27 +
    1.28 +
    1.29 +(*for the "test" target in IsaMakefiles -- signifies successful termination*)
    1.30  fun maketest msg =
    1.31 -  (writeln msg; 
    1.32 -   let val os = TextIO.openOut "test" 
    1.33 -   in  TextIO.output (os, "Test examples ran successfully\n");
    1.34 -       TextIO.closeOut os
    1.35 -   end);
    1.36 +  (writeln msg; write_file "test" "Test examples ran successfully\n");
    1.37  
    1.38  
    1.39  (*print a list surrounded by the brackets lpar and rpar, with comma separator
    1.40 @@ -816,7 +833,7 @@
    1.41    (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
    1.42     writeln ("\n**** Finished " ^ fname ^ " ****")));
    1.43  
    1.44 -(*For Makefiles: use the file, but exit with error code if errors found.*)
    1.45 +(*use the file, but exit with error code if errors found.*)
    1.46  fun exit_use fname = use fname handle _ => exit 1;
    1.47  
    1.48