src/Pure/library.ML
changeset 544 c53386a5bcf1
parent 512 55755ed9fab9
child 955 aa0c5f9daf5b
equal deleted inserted replaced
543:e961b2092869 544:c53386a5bcf1
   645 fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
   645 fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
   646 
   646 
   647 fun assert p msg = if p then () else error msg;
   647 fun assert p msg = if p then () else error msg;
   648 fun deny p msg = if p then error msg else ();
   648 fun deny p msg = if p then error msg else ();
   649 
   649 
       
   650 (*Assert pred for every member of l, generating a message if pred fails*)
       
   651 fun assert_all pred l msg_fn = 
       
   652   let fun asl [] = ()
       
   653 	| asl (x::xs) = if pred x then asl xs
       
   654 	                else error (msg_fn x)
       
   655   in  asl l  end;
   650 
   656 
   651 (* FIXME close file (?) *)
   657 (* FIXME close file (?) *)
   652 (*for the "test" target in Makefiles -- signifies successful termination*)
   658 (*for the "test" target in Makefiles -- signifies successful termination*)
   653 fun maketest msg =
   659 fun maketest msg =
   654   (writeln msg; output (open_out "test", "Test examples ran successfully\n"));
   660   (writeln msg; output (open_out "test", "Test examples ran successfully\n"));