(* Title: Pure/General/output.ML
ID: $Id$
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
Output channels and timing messages.
*)
signature BASIC_OUTPUT =
sig
type output = string
val writeln: string -> unit
val priority: string -> unit
val tracing: string -> unit
val warning: string -> unit
val tolerate_legacy_features: bool ref
val legacy_feature: string -> unit
val cond_timeit: bool -> string -> (unit -> 'a) -> 'a
val timeit: (unit -> 'a) -> 'a
val timeap: ('a -> 'b) -> 'a -> 'b
val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
val timing: bool ref
val time_accumulator: string -> ('a -> 'b) -> 'a -> 'b
end;
signature OUTPUT =
sig
include BASIC_OUTPUT
val default_output: string -> output * int
val default_escape: output -> string
val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
val output_width: string -> output * int
val output: string -> output
val escape: output -> string
val std_output: output -> unit
val std_error: output -> unit
val immediate_output: string -> unit
val writeln_default: output -> unit
val writeln_fn: (output -> unit) ref
val priority_fn: (output -> unit) ref
val tracing_fn: (output -> unit) ref
val warning_fn: (output -> unit) ref
val error_fn: (output -> unit) ref
val debug_fn: (output -> unit) ref
val prompt_fn: (output -> unit) ref
val status_fn: (output -> unit) ref
val error_msg: string -> unit
val prompt: string -> unit
val status: string -> unit
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
val ml_output: (string -> unit) * (string -> 'a)
val accumulated_time: unit -> unit
end;
structure Output: OUTPUT =
struct
(** print modes **)
type output = string; (*raw system output*)
fun default_output s = (s, size s);
fun default_escape (s: output) = s;
local
val default = {output = default_output, escape = default_escape};
val modes = ref (Symtab.make [("", default)]);
in
fun add_mode name output escape = CRITICAL (fn () =>
change modes (Symtab.update_new (name, {output = output, escape = escape})));
fun get_mode () =
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
fun output_width x = #output (get_mode ()) x;
val output = #1 o output_width;
fun escape x = #escape (get_mode ()) x;
(** output channels **)
(* output primitives -- normally NOT used directly!*)
fun std_output s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut));
fun std_error s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr));
val immediate_output = std_output o output;
fun writeln_default "" = ()
| writeln_default s = std_output (suffix "\n" s);
(* Isabelle output channels *)
val writeln_fn = ref writeln_default;
val priority_fn = ref (fn s => ! writeln_fn s);
val tracing_fn = ref (fn s => ! writeln_fn s);
val warning_fn = ref (std_output o suffix "\n" o prefix_lines "### ");
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
val prompt_fn = ref std_output;
val status_fn = ref (fn s => ! writeln_fn s);
fun writeln s = ! writeln_fn (output s);
fun priority s = ! priority_fn (output s);
fun tracing s = ! tracing_fn (output s);
fun warning s = ! warning_fn (output s);
fun error_msg s = ! error_fn (output s);
fun prompt s = ! prompt_fn (output s);
fun status s = ! status_fn (output s);
val tolerate_legacy_features = ref true;
fun legacy_feature s =
(if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
fun no_warnings f = setmp warning_fn (K ()) f;
val debugging = ref false;
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
val ml_output = (writeln, error);
(** timing **)
(*conditional timing with message*)
fun cond_timeit flag msg e =
if flag then
let
val start = start_timing ();
val result = Exn.capture e ();
val end_msg = end_timing start;
val _ = warning (if msg = "" then end_msg else msg ^ "\n" ^ end_msg);
in Exn.release result end
else e ();
(*unconditional timing*)
fun timeit e = cond_timeit true "" e;
(*timed application function*)
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
(*global timing mode*)
val timing = ref false;
(* accumulated timing *)
local
datatype time_info = TI of
{name: string,
timer: Timer.cpu_timer,
sys: Time.time,
usr: Time.time,
gc: Time.time,
count: int};
fun time_init name = ref (TI
{name = name,
timer = Timer.startCPUTimer (),
sys = Time.zeroTime,
usr = Time.zeroTime,
gc = Time.zeroTime,
count = 0});
fun time_reset (r as ref (TI {name, ...})) = r := ! (time_init name);
fun time_check (ref (TI r)) = r;
fun time_add ti f x =
let
fun add_diff time time1 time2 =
Time.+ (time, Time.- (time2, time1) handle Time.Time => Time.zeroTime);
val {name, timer, sys, usr, gc, count} = time_check ti;
val (sys1, usr1, gc1) = check_timer timer;
val result = Exn.capture f x;
val (sys2, usr2, gc2) = check_timer timer;
in
ti := TI
{name = name,
timer = timer,
sys = add_diff sys sys1 sys2,
usr = add_diff usr usr1 usr2,
gc = add_diff gc gc1 gc2,
count = count + 1};
Exn.release result
end;
fun time_finish ti =
let
fun secs prfx time = prfx ^ Time.toString time;
val {name, timer, sys, usr, gc, count} = time_check ti;
in
warning ("Total of " ^ quote name ^ ": " ^
secs "User " usr ^ secs " GC " gc ^ secs " All " (Time.+ (sys, Time.+ (usr, gc))) ^
" secs in " ^ string_of_int count ^ " calls");
time_reset ti
end;
val time_finish_hooks = ref ([]: (unit -> unit) list);
in
fun time_accumulator name =
let val ti = time_init name in
CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
time_add ti
end;
fun accumulated_time () = List.app (fn f => f ()) (! time_finish_hooks);
end;
end;
structure BasicOutput: BASIC_OUTPUT = Output;
open BasicOutput;