src/Pure/library.ML
changeset 1580 e3fd931e6095
parent 1576 af8f43f742a0
child 1592 d89d5ff2397f
equal deleted inserted replaced
1579:688e18023915 1580:e3fd931e6095
   701 
   701 
   702 
   702 
   703 
   703 
   704 (** input / output **)
   704 (** input / output **)
   705 
   705 
   706 fun prs s = output (std_out, s);
   706 val prs_fn = ref(fn s => output (std_out, s));
       
   707 
       
   708 fun prs s = !prs_fn s;
   707 fun writeln s = prs (s ^ "\n");
   709 fun writeln s = prs (s ^ "\n");
   708 
   710 
       
   711 (*print warning*)
       
   712 val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
       
   713 fun warning s = !warning_fn ("Warning: " ^ s);
   709 
   714 
   710 (*print error message and abort to top level*)
   715 (*print error message and abort to top level*)
       
   716 
       
   717 val error_fn = ref(fn s => output (std_out, s ^ "\n"));
       
   718 
   711 exception ERROR;
   719 exception ERROR;
   712 fun error msg = (writeln msg; raise ERROR);
   720 fun error msg = (!error_fn msg; raise ERROR);
   713 fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
   721 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
   714 
   722 
   715 fun assert p msg = if p then () else error msg;
   723 fun assert p msg = if p then () else error msg;
   716 fun deny p msg = if p then error msg else ();
   724 fun deny p msg = if p then error msg else ();
   717 
   725 
   718 (*Assert pred for every member of l, generating a message if pred fails*)
   726 (*Assert pred for every member of l, generating a message if pred fails*)