src/Pure/General/output.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 31685 c124445a4b61
child 32966 5b21661fe618
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@14815
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14815
     3
wenzelm@22585
     4
Output channels and timing messages.
wenzelm@14815
     5
*)
wenzelm@14815
     6
wenzelm@14815
     7
signature BASIC_OUTPUT =
wenzelm@14815
     8
sig
wenzelm@23660
     9
  type output = string
wenzelm@18682
    10
  val writeln: string -> unit
wenzelm@18682
    11
  val priority: string -> unit
wenzelm@18682
    12
  val tracing: string -> unit
wenzelm@18682
    13
  val warning: string -> unit
wenzelm@32738
    14
  val tolerate_legacy_features: bool Unsynchronized.ref
wenzelm@22826
    15
  val legacy_feature: string -> unit
wenzelm@25686
    16
  val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
wenzelm@14815
    17
  val timeit: (unit -> 'a) -> 'a
wenzelm@14815
    18
  val timeap: ('a -> 'b) -> 'a -> 'b
wenzelm@14815
    19
  val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@32738
    20
  val timing: bool Unsynchronized.ref
wenzelm@14815
    21
end;
wenzelm@14815
    22
wenzelm@14815
    23
signature OUTPUT =
wenzelm@14815
    24
sig
wenzelm@14815
    25
  include BASIC_OUTPUT
wenzelm@23660
    26
  val default_output: string -> output * int
wenzelm@23660
    27
  val default_escape: output -> string
wenzelm@23660
    28
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
wenzelm@23660
    29
  val output_width: string -> output * int
wenzelm@23660
    30
  val output: string -> output
wenzelm@23660
    31
  val escape: output -> string
wenzelm@23660
    32
  val std_output: output -> unit
wenzelm@23660
    33
  val std_error: output -> unit
wenzelm@23660
    34
  val writeln_default: output -> unit
wenzelm@32738
    35
  val writeln_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    36
  val priority_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    37
  val tracing_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    38
  val warning_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    39
  val error_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    40
  val debug_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    41
  val prompt_fn: (output -> unit) Unsynchronized.ref
wenzelm@32738
    42
  val status_fn: (output -> unit) Unsynchronized.ref
wenzelm@25845
    43
  val error_msg: string -> unit
wenzelm@25845
    44
  val prompt: string -> unit
wenzelm@27605
    45
  val status: string -> unit
wenzelm@32738
    46
  val debugging: bool Unsynchronized.ref
wenzelm@22585
    47
  val no_warnings: ('a -> 'b) -> 'a -> 'b
wenzelm@22130
    48
  val debug: (unit -> string) -> unit
wenzelm@14815
    49
end;
wenzelm@14815
    50
wenzelm@14815
    51
structure Output: OUTPUT =
wenzelm@14815
    52
struct
wenzelm@14815
    53
wenzelm@23616
    54
(** print modes **)
wenzelm@14881
    55
wenzelm@23660
    56
type output = string;  (*raw system output*)
wenzelm@23660
    57
wenzelm@23616
    58
fun default_output s = (s, size s);
wenzelm@23660
    59
fun default_escape (s: output) = s;
wenzelm@14815
    60
wenzelm@23616
    61
local
wenzelm@23616
    62
  val default = {output = default_output, escape = default_escape};
wenzelm@32738
    63
  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
wenzelm@23616
    64
in
wenzelm@23922
    65
  fun add_mode name output escape = CRITICAL (fn () =>
wenzelm@32738
    66
    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
wenzelm@23616
    67
  fun get_mode () =
wenzelm@24612
    68
    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
wenzelm@23616
    69
end;
wenzelm@14815
    70
wenzelm@19265
    71
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    72
val output = #1 o output_width;
wenzelm@23727
    73
wenzelm@23616
    74
fun escape x = #escape (get_mode ()) x;
wenzelm@14815
    75
wenzelm@14815
    76
wenzelm@14815
    77
wenzelm@14815
    78
(** output channels **)
wenzelm@14815
    79
wenzelm@14984
    80
(* output primitives -- normally NOT used directly!*)
wenzelm@14984
    81
wenzelm@24058
    82
fun std_output s = NAMED_CRITICAL "IO" (fn () =>
wenzelm@23922
    83
  (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
wenzelm@23922
    84
wenzelm@24058
    85
fun std_error s = NAMED_CRITICAL "IO" (fn () =>
wenzelm@23922
    86
  (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
wenzelm@14815
    87
wenzelm@27605
    88
fun writeln_default "" = ()
wenzelm@27605
    89
  | writeln_default s = std_output (suffix "\n" s);
wenzelm@14815
    90
wenzelm@14984
    91
wenzelm@14984
    92
(* Isabelle output channels *)
wenzelm@14984
    93
wenzelm@32738
    94
val writeln_fn = Unsynchronized.ref writeln_default;
wenzelm@32738
    95
val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@32738
    96
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@32738
    97
val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
wenzelm@32738
    98
val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
wenzelm@32738
    99
val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
wenzelm@32738
   100
val prompt_fn = Unsynchronized.ref std_output;
wenzelm@32738
   101
val status_fn = Unsynchronized.ref (fn _: string => ());
wenzelm@14815
   102
wenzelm@14815
   103
fun writeln s = ! writeln_fn (output s);
wenzelm@14815
   104
fun priority s = ! priority_fn (output s);
wenzelm@14815
   105
fun tracing s = ! tracing_fn (output s);
wenzelm@14815
   106
fun warning s = ! warning_fn (output s);
wenzelm@25845
   107
fun error_msg s = ! error_fn (output s);
wenzelm@25845
   108
fun prompt s = ! prompt_fn (output s);
wenzelm@27605
   109
fun status s = ! status_fn (output s);
aspinall@15190
   110
wenzelm@32738
   111
val tolerate_legacy_features = Unsynchronized.ref true;
wenzelm@22826
   112
fun legacy_feature s =
wenzelm@26291
   113
  (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
wenzelm@22826
   114
wenzelm@16191
   115
fun no_warnings f = setmp warning_fn (K ()) f;
wenzelm@16191
   116
wenzelm@32738
   117
val debugging = Unsynchronized.ref false;
wenzelm@22130
   118
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
aspinall@15190
   119
wenzelm@14815
   120
wenzelm@14815
   121
wenzelm@14815
   122
(** timing **)
wenzelm@14815
   123
wenzelm@25686
   124
(*conditional timing with message*)
wenzelm@25686
   125
fun cond_timeit flag msg e =
wenzelm@14815
   126
  if flag then
wenzelm@23862
   127
    let
wenzelm@23862
   128
      val start = start_timing ();
wenzelm@25686
   129
      val result = Exn.capture e ();
wenzelm@30187
   130
      val end_msg = #message (end_timing start);
wenzelm@25686
   131
      val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
wenzelm@25686
   132
    in Exn.release result end
wenzelm@25686
   133
  else e ();
haftmann@25667
   134
wenzelm@23862
   135
(*unconditional timing*)
wenzelm@25686
   136
fun timeit e = cond_timeit true "" e;
wenzelm@14815
   137
wenzelm@14815
   138
(*timed application function*)
wenzelm@14815
   139
fun timeap f x = timeit (fn () => f x);
wenzelm@25686
   140
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
wenzelm@25686
   141
wenzelm@25686
   142
(*global timing mode*)
wenzelm@32738
   143
val timing = Unsynchronized.ref false;
wenzelm@14815
   144
wenzelm@14815
   145
end;
wenzelm@14815
   146
wenzelm@32738
   147
structure Basic_Output: BASIC_OUTPUT = Output;
wenzelm@32738
   148
open Basic_Output;