src/Pure/General/output.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24652 22b657bee22d
child 25640 1546ffd84986
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/output.ML
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     4
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
     5
Output channels and timing messages.
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     6
*)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     7
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     8
signature BASIC_OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
     9
sig
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    10
  type output = string
18682
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
    11
  val writeln: string -> unit
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
    12
  val priority: string -> unit
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
    13
  val tracing: string -> unit
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
    14
  val warning: string -> unit
22826
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
    15
  val tolerate_legacy_features: bool ref
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
    16
  val legacy_feature: string -> unit
14869
544be18288e6 moved exception handling back to library.ML;
wenzelm
parents: 14862
diff changeset
    17
  val timing: bool ref
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    18
  val cond_timeit: bool -> (unit -> 'a) -> 'a
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    19
  val timeit: (unit -> 'a) -> 'a
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    20
  val timeap: ('a -> 'b) -> 'a -> 'b
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    21
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
    22
  val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    23
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    24
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    25
signature OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    26
sig
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    27
  include BASIC_OUTPUT
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    28
  val default_output: string -> output * int
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    29
  val default_escape: output -> string
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    30
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    31
  val output_width: string -> output * int
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    32
  val output: string -> output
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    33
  val escape: output -> string
23727
39f8d1480d55 added escape_malformed (failsafe);
wenzelm
parents: 23660
diff changeset
    34
  val escape_malformed: string -> string
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    35
  val std_output: output -> unit
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    36
  val std_error: output -> unit
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
    37
  val immediate_output: string -> unit
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    38
  val writeln_default: output -> unit
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    39
  val writeln_fn: (output -> unit) ref
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    40
  val priority_fn: (output -> unit) ref
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    41
  val tracing_fn: (output -> unit) ref
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    42
  val warning_fn: (output -> unit) ref
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    43
  val error_fn: (output -> unit) ref
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    44
  val debug_fn: (output -> unit) ref
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
    45
  val debugging: bool ref
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
    46
  val no_warnings: ('a -> 'b) -> 'a -> 'b
22130
0906fd95e0b5 Output.debug: non-strict;
wenzelm
parents: 21336
diff changeset
    47
  val debug: (unit -> string) -> unit
18682
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
    48
  val error_msg: string -> unit
24652
22b657bee22d ml_output: proper error instead of error_msg;
wenzelm
parents: 24612
diff changeset
    49
  val ml_output: (string -> unit) * (string -> 'a)
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
    50
  val accumulated_time: unit -> unit
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    51
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    52
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    53
structure Output: OUTPUT =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    54
struct
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    55
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    56
(** print modes **)
14881
e1f501a14159 added has_mode; handle_error: output raw;
wenzelm
parents: 14869
diff changeset
    57
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    58
type output = string;  (*raw system output*)
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    59
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    60
fun default_output s = (s, size s);
23660
18765718cf62 type output = string indicates raw system output;
wenzelm
parents: 23616
diff changeset
    61
fun default_escape (s: output) = s;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    62
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    63
local
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    64
  val default = {output = default_output, escape = default_escape};
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    65
  val modes = ref (Symtab.make [("", default)]);
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    66
in
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23862
diff changeset
    67
  fun add_mode name output escape = CRITICAL (fn () =>
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23862
diff changeset
    68
    change modes (Symtab.update_new (name, {output = output, escape = escape})));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    69
  fun get_mode () =
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24058
diff changeset
    70
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    71
end;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    72
19265
cae36e16f3c0 Output.add_mode: keyword component;
wenzelm
parents: 18716
diff changeset
    73
fun output_width x = #output (get_mode ()) x;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    74
val output = #1 o output_width;
23727
39f8d1480d55 added escape_malformed (failsafe);
wenzelm
parents: 23660
diff changeset
    75
23616
ba6deff7d214 renamed raw to escape;
wenzelm
parents: 22826
diff changeset
    76
fun escape x = #escape (get_mode ()) x;
23727
39f8d1480d55 added escape_malformed (failsafe);
wenzelm
parents: 23660
diff changeset
    77
val escape_malformed = escape o translate_string output;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    78
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    79
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    80
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    81
(** output channels **)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    82
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    83
(* output primitives -- normally NOT used directly!*)
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    84
24058
81aafd465662 NAMED_CRITICAL;
wenzelm
parents: 24054
diff changeset
    85
fun std_output s = NAMED_CRITICAL "IO" (fn () =>
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23862
diff changeset
    86
  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23862
diff changeset
    87
24058
81aafd465662 NAMED_CRITICAL;
wenzelm
parents: 24054
diff changeset
    88
fun std_error s = NAMED_CRITICAL "IO" (fn () =>
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 23862
diff changeset
    89
  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    90
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    91
val immediate_output = std_output o output;
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    92
val writeln_default = std_output o suffix "\n";
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    93
14984
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    94
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    95
(* Isabelle output channels *)
edbc81e60809 immediate_output;
wenzelm
parents: 14978
diff changeset
    96
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    97
val writeln_fn = ref writeln_default;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    98
val priority_fn = ref (fn s => ! writeln_fn s);
77a509d83163 output channels;
wenzelm
parents:
diff changeset
    99
val tracing_fn = ref (fn s => ! writeln_fn s);
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   100
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   101
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
15190
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   102
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   103
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   104
fun writeln s = ! writeln_fn (output s);
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   105
fun priority s = ! priority_fn (output s);
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   106
fun tracing s = ! tracing_fn (output s);
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   107
fun warning s = ! warning_fn (output s);
15190
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   108
22826
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
   109
val tolerate_legacy_features = ref true;
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
   110
fun legacy_feature s =
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
   111
  (if ! tolerate_legacy_features then warning else error) ("Legacy feature: " ^ s);
0f4c501a691e explicit treatment of legacy_features;
wenzelm
parents: 22699
diff changeset
   112
16191
9d503d6fcbb1 added no_warnings;
wenzelm
parents: 15531
diff changeset
   113
fun no_warnings f = setmp warning_fn (K ()) f;
9d503d6fcbb1 added no_warnings;
wenzelm
parents: 15531
diff changeset
   114
22130
0906fd95e0b5 Output.debug: non-strict;
wenzelm
parents: 21336
diff changeset
   115
val debugging = ref false;
0906fd95e0b5 Output.debug: non-strict;
wenzelm
parents: 21336
diff changeset
   116
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
15190
b6788dbd2ef9 Add info and debug output channels.
aspinall
parents: 15010
diff changeset
   117
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   118
fun error_msg s = ! error_fn (output s);
18682
216692feebab removed special ERROR handling stuff (transform_error etc.);
wenzelm
parents: 17539
diff changeset
   119
24652
22b657bee22d ml_output: proper error instead of error_msg;
wenzelm
parents: 24612
diff changeset
   120
val ml_output = (writeln, error);
20926
b2f67b947200 moved Context.ml_output to Output.ml_output;
wenzelm
parents: 20664
diff changeset
   121
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   122
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   123
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   124
(** timing **)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   125
14869
544be18288e6 moved exception handling back to library.ML;
wenzelm
parents: 14862
diff changeset
   126
(*global timing mode*)
544be18288e6 moved exception handling back to library.ML;
wenzelm
parents: 14862
diff changeset
   127
val timing = ref false;
544be18288e6 moved exception handling back to library.ML;
wenzelm
parents: 14862
diff changeset
   128
23862
wenzelm
parents: 23727
diff changeset
   129
(*conditional timing*)
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   130
fun cond_timeit flag f =
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   131
  if flag then
23862
wenzelm
parents: 23727
diff changeset
   132
    let
wenzelm
parents: 23727
diff changeset
   133
      val start = start_timing ();
wenzelm
parents: 23727
diff changeset
   134
      val result = f ();
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
   135
    in warning (end_timing start); result end
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   136
  else f ();
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   137
23862
wenzelm
parents: 23727
diff changeset
   138
(*unconditional timing*)
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   139
fun timeit x = cond_timeit true x;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   140
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   141
(*timed application function*)
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   142
fun timeap f x = timeit (fn () => f x);
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
   143
fun timeap_msg s f x = (warning s; timeap f x);
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   144
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   145
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   146
(* accumulated timing *)
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   147
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   148
local
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   149
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   150
datatype time_info = TI of
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   151
  {name: string,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   152
   timer: Timer.cpu_timer,
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   153
   sys: Time.time,
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   154
   usr: Time.time,
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   155
   gc: Time.time,
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   156
   count: int};
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   157
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   158
fun time_init name = ref (TI
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   159
 {name = name,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   160
  timer = Timer.startCPUTimer (),
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   161
  sys = Time.zeroTime,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   162
  usr = Time.zeroTime,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   163
  gc = Time.zeroTime,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   164
  count = 0});
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   165
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   166
fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   167
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   168
fun time_check (ref (TI r)) = r;
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   169
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   170
fun time_add ti f x =
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   171
  let
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   172
    fun add_diff time time1 time2 =
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   173
      Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   174
    val {name, timer, sys, usr, gc, count} = time_check ti;
21295
63552bc99cfb tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 20926
diff changeset
   175
    val (sys1, usr1, gc1) = check_timer timer;
23963
c2ee97a963db moved exception capture/release to structure Exn;
wenzelm
parents: 23939
diff changeset
   176
    val result = Exn.capture f x;
21295
63552bc99cfb tuned names of start_timing,/end_timing/check_timer;
wenzelm
parents: 20926
diff changeset
   177
    val (sys2, usr2, gc2) = check_timer timer;
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   178
  in
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   179
    ti := TI
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   180
     {name = name,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   181
      timer = timer,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   182
      sys = add_diff sys sys1 sys2,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   183
      usr = add_diff usr usr1 usr2,
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   184
      gc = add_diff gc gc1 gc2,
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   185
      count = count + 1};
23963
c2ee97a963db moved exception capture/release to structure Exn;
wenzelm
parents: 23939
diff changeset
   186
    Exn.release result
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   187
  end;
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   188
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   189
fun time_finish ti =
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   190
  let
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   191
    fun secs prfx time = prfx ^ Time.toString time;
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   192
    val {name, timer, sys, usr, gc, count} = time_check ti;
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   193
  in
22585
16af5cb012e7 cleaned-up Output functions;
wenzelm
parents: 22469
diff changeset
   194
    warning ("Total of " ^ quote name ^ ": " ^
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   195
      secs "User " usr ^ secs "  GC " gc ^ secs "  All " (Time.+ (sys, Time.+ (usr, gc))) ^
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   196
      " secs in " ^ string_of_int count ^ " calls");
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   197
    time_reset ti
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   198
  end;
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   199
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   200
val time_finish_hooks = ref ([]: (unit -> unit) list);
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   201
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   202
in
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   203
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   204
fun time_accumulator name =
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   205
  let val ti = time_init name in
23939
e543359fe8b6 marked some CRITICAL sections;
wenzelm
parents: 23922
diff changeset
   206
    CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
16726
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   207
    time_add ti
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   208
  end;
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   209
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   210
fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
4399016bf13e added time_accumulator and accumulated_time supercede
wenzelm
parents: 16683
diff changeset
   211
14978
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   212
end;
108ce0289c35 added accumulated timing;
wenzelm
parents: 14955
diff changeset
   213
14815
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   214
end;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   215
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   216
structure BasicOutput: BASIC_OUTPUT = Output;
77a509d83163 output channels;
wenzelm
parents:
diff changeset
   217
open BasicOutput;