src/Pure/library.ML
changeset 3624 36e19fce289e
parent 3606 5d7073700fbc
child 3645 cfbd814a11f2
equal deleted inserted replaced
3623:e843c1d6f9e1 3624:36e19fce289e
   768   let fun asl [] = ()
   768   let fun asl [] = ()
   769         | asl (x::xs) = if pred x then asl xs
   769         | asl (x::xs) = if pred x then asl xs
   770                         else error (msg_fn x)
   770                         else error (msg_fn x)
   771   in  asl l  end;
   771   in  asl l  end;
   772 
   772 
   773 (*for the "test" target in Makefiles -- signifies successful termination*)
   773 
       
   774 (* read / write files *)
       
   775 
       
   776 fun read_file name =
       
   777   let
       
   778     val instream  = TextIO.openIn name;
       
   779     val intext = TextIO.inputAll instream;
       
   780   in
       
   781     TextIO.closeIn instream;
       
   782     intext
       
   783   end;
       
   784 
       
   785 fun write_file name txt =
       
   786   let
       
   787     val outstream = TextIO.openOut name;
       
   788   in
       
   789     TextIO.output (outstream, txt);
       
   790     TextIO.closeOut outstream
       
   791   end;
       
   792 
       
   793 
       
   794 (*for the "test" target in IsaMakefiles -- signifies successful termination*)
   774 fun maketest msg =
   795 fun maketest msg =
   775   (writeln msg; 
   796   (writeln msg; write_file "test" "Test examples ran successfully\n");
   776    let val os = TextIO.openOut "test" 
       
   777    in  TextIO.output (os, "Test examples ran successfully\n");
       
   778        TextIO.closeOut os
       
   779    end);
       
   780 
   797 
   781 
   798 
   782 (*print a list surrounded by the brackets lpar and rpar, with comma separator
   799 (*print a list surrounded by the brackets lpar and rpar, with comma separator
   783   print nothing for empty list*)
   800   print nothing for empty list*)
   784 fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
   801 fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
   814 (*timed "use" function, printing filenames*)
   831 (*timed "use" function, printing filenames*)
   815 fun time_use fname = timeit (fn () =>
   832 fun time_use fname = timeit (fn () =>
   816   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
   833   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
   817    writeln ("\n**** Finished " ^ fname ^ " ****")));
   834    writeln ("\n**** Finished " ^ fname ^ " ****")));
   818 
   835 
   819 (*For Makefiles: use the file, but exit with error code if errors found.*)
   836 (*use the file, but exit with error code if errors found.*)
   820 fun exit_use fname = use fname handle _ => exit 1;
   837 fun exit_use fname = use fname handle _ => exit 1;
   821 
   838 
   822 
   839 
   823 (** filenames and paths **)
   840 (** filenames and paths **)
   824 
   841