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