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