src/Pure/library.ML
changeset 3553 a148c7e7152e
parent 3525 88edd3450460
child 3606 5d7073700fbc
equal deleted inserted replaced
3552:f348e8a2db4b 3553:a148c7e7152e
   754 
   754 
   755 fun warning s = !warning_fn s;
   755 fun warning s = !warning_fn s;
   756 
   756 
   757 (*print error message and abort to top level*)
   757 (*print error message and abort to top level*)
   758 exception ERROR;
   758 exception ERROR;
   759 fun error s = (!error_fn s; raise ERROR);
   759 fun error_msg s = !error_fn s;
   760 fun sys_error msg = (!error_fn " !! SYSTEM ERROR !!\n"; error msg);
   760 fun error s = (error_msg s; raise ERROR);
       
   761 fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
   761 
   762 
   762 fun assert p msg = if p then () else error msg;
   763 fun assert p msg = if p then () else error msg;
   763 fun deny p msg = if p then error msg else ();
   764 fun deny p msg = if p then error msg else ();
   764 
   765 
   765 (*Assert pred for every member of l, generating a message if pred fails*)
   766 (*Assert pred for every member of l, generating a message if pred fails*)