maketest now closes the output file
authorpaulson
Wed Mar 20 18:40:57 1996 +0100 (1996-03-20)
changeset 1592d89d5ff2397f
parent 1591 7fa0265dcd13
child 1593 69ed69a9c32a
maketest now closes the output file
Declared type mtree for proof objects
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Mar 20 18:39:59 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Mar 20 18:40:57 1996 +0100
     1.3 @@ -730,10 +730,13 @@
     1.4  	                else error (msg_fn x)
     1.5    in  asl l  end;
     1.6  
     1.7 -(* FIXME close file (?) *)
     1.8  (*for the "test" target in Makefiles -- signifies successful termination*)
     1.9  fun maketest msg =
    1.10 -  (writeln msg; output (open_out "test", "Test examples ran successfully\n"));
    1.11 +  (writeln msg; 
    1.12 +   let val os = open_out "test" 
    1.13 +   in  output (os, "Test examples ran successfully\n");
    1.14 +       close_out os
    1.15 +   end);
    1.16  
    1.17  
    1.18  (*print a list surrounded by the brackets lpar and rpar, with comma separator
    1.19 @@ -946,4 +949,7 @@
    1.20  
    1.21  end;
    1.22  
    1.23 +(*Variable-branching trees: for proof terms*)
    1.24 +datatype 'a mtree = Join of 'a * 'a mtree list;
    1.25 +
    1.26  open Library;