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