src/Pure/library.ML
changeset 3525 88edd3450460
parent 3407 afd288caf573
child 3553 a148c7e7152e
equal deleted inserted replaced
3524:c02cb15830de 3525:88edd3450460
   721   else if a = b then EQUAL
   721   else if a = b then EQUAL
   722   else GREATER;
   722   else GREATER;
   723 
   723 
   724 
   724 
   725 
   725 
   726 (** input / output **)
   726 (** input / output and diagnostics **)
   727 
   727 
   728 val cd = OS.FileSys.chDir;
   728 val cd = OS.FileSys.chDir;
   729 val pwd = OS.FileSys.getDir;
   729 val pwd = OS.FileSys.getDir;
   730 
   730 
   731 val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
   731 
       
   732 local
       
   733   fun out s =
       
   734     (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
       
   735 
       
   736   fun lines cs =
       
   737     (case take_prefix (not_equal "\n") cs of
       
   738       (cs', []) => [implode cs']
       
   739     | (cs', _ :: cs'') => implode cs' :: lines cs'');
       
   740 
       
   741   fun prefix_lines prfx txt =
       
   742     txt |> explode |> lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
       
   743 in
       
   744 
       
   745 (*hooks for output channels: normal, warning, error*)
       
   746 val prs_fn = ref (fn s => out s);
       
   747 val warning_fn = ref (fn s => out (prefix_lines "### " s));
       
   748 val error_fn = ref (fn s => out (prefix_lines "*** " s));
       
   749 
       
   750 end;
   732 
   751 
   733 fun prs s = !prs_fn s;
   752 fun prs s = !prs_fn s;
   734 fun writeln s = prs (s ^ "\n");
   753 fun writeln s = prs (s ^ "\n");
   735 
   754 
   736 (* TextIO.output to LaTeX / xdvi *)
   755 fun warning s = !warning_fn s;
   737 fun latex s = 
       
   738         execute ( "( cd /tmp ; echo \"" ^ s ^
       
   739         "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
       
   740 
       
   741 (*print warning*)
       
   742 val warning_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
       
   743 fun warning s = !warning_fn ("Warning: " ^ s);
       
   744 
   756 
   745 (*print error message and abort to top level*)
   757 (*print error message and abort to top level*)
   746 
       
   747 val error_fn = ref(fn s => TextIO.output 
       
   748 		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
       
   749 
       
   750 exception ERROR;
   758 exception ERROR;
   751 fun error msg = (!error_fn msg;
   759 fun error s = (!error_fn s; raise ERROR);
   752 		 TextIO.flushOut TextIO.stdOut; 
   760 fun sys_error msg = (!error_fn " !! SYSTEM ERROR !!\n"; error msg);
   753 		 raise ERROR);
       
   754 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
       
   755 
   761 
   756 fun assert p msg = if p then () else error msg;
   762 fun assert p msg = if p then () else error msg;
   757 fun deny p msg = if p then error msg else ();
   763 fun deny p msg = if p then error msg else ();
   758 
   764 
   759 (*Assert pred for every member of l, generating a message if pred fails*)
   765 (*Assert pred for every member of l, generating a message if pred fails*)
   787   seq (fn x => (pre x; writeln ""));
   793   seq (fn x => (pre x; writeln ""));
   788 
   794 
   789 
   795 
   790 val print_int = prs o string_of_int;
   796 val print_int = prs o string_of_int;
   791 
   797 
       
   798 
       
   799 (* output to LaTeX / xdvi *)
       
   800 fun latex s =
       
   801   execute ("( cd /tmp ; echo \"" ^ s ^
       
   802     "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
   792 
   803 
   793 
   804 
   794 (** timing **)
   805 (** timing **)
   795 
   806 
   796 (*unconditional timing function*)
   807 (*unconditional timing function*)