improved output channels: normal, warning, error;
authorwenzelm
Fri Jul 18 13:33:20 1997 +0200 (1997-07-18)
changeset 352588edd3450460
parent 3524 c02cb15830de
child 3526 df4d0dad2b4e
improved output channels: normal, warning, error;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Jul 17 15:03:38 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Jul 18 13:33:20 1997 +0200
     1.3 @@ -723,35 +723,41 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** input / output **)
     1.8 +(** input / output and diagnostics **)
     1.9  
    1.10  val cd = OS.FileSys.chDir;
    1.11  val pwd = OS.FileSys.getDir;
    1.12  
    1.13 -val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
    1.14 +
    1.15 +local
    1.16 +  fun out s =
    1.17 +    (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.18 +
    1.19 +  fun lines cs =
    1.20 +    (case take_prefix (not_equal "\n") cs of
    1.21 +      (cs', []) => [implode cs']
    1.22 +    | (cs', _ :: cs'') => implode cs' :: lines cs'');
    1.23 +
    1.24 +  fun prefix_lines prfx txt =
    1.25 +    txt |> explode |> lines |> map (fn s => prfx ^ s ^ "\n") |> implode;
    1.26 +in
    1.27 +
    1.28 +(*hooks for output channels: normal, warning, error*)
    1.29 +val prs_fn = ref (fn s => out s);
    1.30 +val warning_fn = ref (fn s => out (prefix_lines "### " s));
    1.31 +val error_fn = ref (fn s => out (prefix_lines "*** " s));
    1.32 +
    1.33 +end;
    1.34  
    1.35  fun prs s = !prs_fn s;
    1.36  fun writeln s = prs (s ^ "\n");
    1.37  
    1.38 -(* TextIO.output to LaTeX / xdvi *)
    1.39 -fun latex s = 
    1.40 -        execute ( "( cd /tmp ; echo \"" ^ s ^
    1.41 -        "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
    1.42 -
    1.43 -(*print warning*)
    1.44 -val warning_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
    1.45 -fun warning s = !warning_fn ("Warning: " ^ s);
    1.46 +fun warning s = !warning_fn s;
    1.47  
    1.48  (*print error message and abort to top level*)
    1.49 -
    1.50 -val error_fn = ref(fn s => TextIO.output 
    1.51 -		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
    1.52 -
    1.53  exception ERROR;
    1.54 -fun error msg = (!error_fn msg;
    1.55 -		 TextIO.flushOut TextIO.stdOut; 
    1.56 -		 raise ERROR);
    1.57 -fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
    1.58 +fun error s = (!error_fn s; raise ERROR);
    1.59 +fun sys_error msg = (!error_fn " !! SYSTEM ERROR !!\n"; error msg);
    1.60  
    1.61  fun assert p msg = if p then () else error msg;
    1.62  fun deny p msg = if p then error msg else ();
    1.63 @@ -790,6 +796,11 @@
    1.64  val print_int = prs o string_of_int;
    1.65  
    1.66  
    1.67 +(* output to LaTeX / xdvi *)
    1.68 +fun latex s =
    1.69 +  execute ("( cd /tmp ; echo \"" ^ s ^
    1.70 +    "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &");
    1.71 +
    1.72  
    1.73  (** timing **)
    1.74