src/Pure/General/output.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23862 b1861768d8f4
child 23922 707639e9497d
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/output.ML
     2     ID:         $Id$
     3     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     4 
     5 Output channels and timing messages.
     6 *)
     7 
     8 signature BASIC_OUTPUT =
     9 sig
    10   type output = string
    11   val writeln: string -> unit
    12   val priority: string -> unit
    13   val tracing: string -> unit
    14   val warning: string -> unit
    15   val tolerate_legacy_features: bool ref
    16   val legacy_feature: string -> unit
    17   val timing: bool ref
    18   val cond_timeit: bool -> (unit -> 'a) -> 'a
    19   val timeit: (unit -> 'a) -> 'a
    20   val timeap: ('a -> 'b) -> 'a -> 'b
    21   val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    22   val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
    23 end;
    24 
    25 signature OUTPUT =
    26 sig
    27   include BASIC_OUTPUT
    28   val default_output: string -> output * int
    29   val default_escape: output -> string
    30   val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
    31   val output_width: string -> output * int
    32   val output: string -> output
    33   val escape: output -> string
    34   val escape_malformed: string -> string
    35   val std_output: output -> unit
    36   val std_error: output -> unit
    37   val immediate_output: string -> unit
    38   val writeln_default: output -> unit
    39   val writeln_fn: (output -> unit) ref
    40   val priority_fn: (output -> unit) ref
    41   val tracing_fn: (output -> unit) ref
    42   val warning_fn: (output -> unit) ref
    43   val error_fn: (output -> unit) ref
    44   val debug_fn: (output -> unit) ref
    45   val debugging: bool ref
    46   val no_warnings: ('a -> 'b) -> 'a -> 'b
    47   exception TOPLEVEL_ERROR
    48   val do_toplevel_errors: bool ref
    49   val toplevel_errors: ('a -> 'b) -> 'a -> 'b
    50   val ML_errors: ('a -> 'b) -> 'a -> 'b
    51   val debug: (unit -> string) -> unit
    52   val error_msg: string -> unit
    53   val ml_output: (string -> unit) * (string -> unit)
    54   val accumulated_time: unit -> unit
    55 end;
    56 
    57 structure Output: OUTPUT =
    58 struct
    59 
    60 (** print modes **)
    61 
    62 type output = string;  (*raw system output*)
    63 
    64 fun default_output s = (s, size s);
    65 fun default_escape (s: output) = s;
    66 
    67 local
    68   val default = {output = default_output, escape = default_escape};
    69   val modes = ref (Symtab.make [("", default)]);
    70 in
    71   fun add_mode name output escape =
    72     change modes (Symtab.update_new (name, {output = output, escape = escape}));
    73   fun get_mode () =
    74     the_default default (Library.get_first (Symtab.lookup (! modes)) (! print_mode));
    75 end;
    76 
    77 fun output_width x = #output (get_mode ()) x;
    78 val output = #1 o output_width;
    79 
    80 fun escape x = #escape (get_mode ()) x;
    81 val escape_malformed = escape o translate_string output;
    82 
    83 
    84 
    85 (** output channels **)
    86 
    87 (* output primitives -- normally NOT used directly!*)
    88 
    89 fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    90 fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    91 
    92 val immediate_output = std_output o output;
    93 val writeln_default = std_output o suffix "\n";
    94 
    95 
    96 (* Isabelle output channels *)
    97 
    98 val writeln_fn = ref writeln_default;
    99 val priority_fn = ref (fn s => ! writeln_fn s);
   100 val tracing_fn = ref (fn s => ! writeln_fn s);
   101 val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
   102 val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
   103 val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
   104 
   105 fun writeln s = ! writeln_fn (output s);
   106 fun priority s = ! priority_fn (output s);
   107 fun tracing s = ! tracing_fn (output s);
   108 fun warning s = ! warning_fn (output s);
   109 
   110 val tolerate_legacy_features = ref true;
   111 fun legacy_feature s =
   112   (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
   113 
   114 fun no_warnings f = setmp warning_fn (K ()) f;
   115 
   116 val debugging = ref false;
   117 fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
   118 
   119 fun error_msg s = ! error_fn (output s);
   120 
   121 val ml_output = (writeln, error_msg);
   122 
   123 
   124 (* toplevel errors *)
   125 
   126 exception TOPLEVEL_ERROR;
   127 
   128 val do_toplevel_errors = ref true;
   129 
   130 fun toplevel_errors f x =
   131   if ! do_toplevel_errors then
   132     f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
   133   else f x;
   134 
   135 fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
   136 
   137 
   138 
   139 (** timing **)
   140 
   141 (*global timing mode*)
   142 val timing = ref false;
   143 
   144 (*conditional timing*)
   145 fun cond_timeit flag f =
   146   if flag then
   147     let
   148       val start = start_timing ();
   149       val result = f ();
   150     in warning (end_timing start); result end
   151   else f ();
   152 
   153 (*unconditional timing*)
   154 fun timeit x = cond_timeit true x;
   155 
   156 (*timed application function*)
   157 fun timeap f x = timeit (fn () => f x);
   158 fun timeap_msg s f x = (warning s; timeap f x);
   159 
   160 
   161 (* accumulated timing *)
   162 
   163 local
   164 
   165 datatype time_info = TI of
   166   {name: string,
   167    timer: Timer.cpu_timer,
   168    sys: Time.time,
   169    usr: Time.time,
   170    gc: Time.time,
   171    count: int};
   172 
   173 fun time_init name = ref (TI
   174  {name = name,
   175   timer = Timer.startCPUTimer (),
   176   sys = Time.zeroTime,
   177   usr = Time.zeroTime,
   178   gc = Time.zeroTime,
   179   count = 0});
   180 
   181 fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
   182 
   183 fun time_check (ref (TI r)) = r;
   184 
   185 fun time_add ti f x =
   186   let
   187     fun add_diff time time1 time2 =
   188       Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
   189     val {name, timer, sys, usr, gc, count} = time_check ti;
   190     val (sys1, usr1, gc1) = check_timer timer;
   191     val result = capture f x;
   192     val (sys2, usr2, gc2) = check_timer timer;
   193   in
   194     ti := TI
   195      {name = name,
   196       timer = timer,
   197       sys = add_diff sys sys1 sys2,
   198       usr = add_diff usr usr1 usr2,
   199       gc = add_diff gc gc1 gc2,
   200       count = count + 1};
   201     release result
   202   end;
   203 
   204 fun time_finish ti =
   205   let
   206     fun secs prfx time = prfx ^ Time.toString time;
   207     val {name, timer, sys, usr, gc, count} = time_check ti;
   208   in
   209     warning ("Total of " ^ quote name ^ ": " ^
   210       secs "User " usr ^ secs "  GC " gc ^ secs "  All " (Time.+ (sys, Time.+ (usr, gc))) ^
   211       " secs in " ^ string_of_int count ^ " calls");
   212     time_reset ti
   213   end;
   214 
   215 val time_finish_hooks = ref ([]: (unit -> unit) list);
   216 
   217 in
   218 
   219 fun time_accumulator name =
   220   let val ti = time_init name in
   221     change time_finish_hooks (cons (fn () => time_finish ti));
   222     time_add ti
   223   end;
   224 
   225 fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
   226 
   227 end;
   228 
   229 end;
   230 
   231 structure BasicOutput: BASIC_OUTPUT = Output;
   232 open BasicOutput;