src/Pure/General/output.ML
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
parent 43746 a41f618c641d
child 43760 ef8375a4dae4
permissions -rw-r--r--
JVM method invocation service via Scala layer;
wenzelm@14815
     1
(*  Title:      Pure/General/output.ML
wenzelm@14815
     2
    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
wenzelm@14815
     3
wenzelm@42012
     4
Isabelle output channels.
wenzelm@14815
     5
*)
wenzelm@14815
     6
wenzelm@14815
     7
signature BASIC_OUTPUT =
wenzelm@14815
     8
sig
wenzelm@18682
     9
  val writeln: string -> unit
wenzelm@18682
    10
  val tracing: string -> unit
wenzelm@18682
    11
  val warning: string -> unit
wenzelm@22826
    12
  val legacy_feature: string -> unit
wenzelm@14815
    13
end;
wenzelm@14815
    14
wenzelm@14815
    15
signature OUTPUT =
wenzelm@14815
    16
sig
wenzelm@14815
    17
  include BASIC_OUTPUT
wenzelm@40131
    18
  type output = string
wenzelm@23660
    19
  val default_output: string -> output * int
wenzelm@23660
    20
  val default_escape: output -> string
wenzelm@23660
    21
  val add_mode: string -> (string -> output * int) -> (output -> string) -> unit
wenzelm@23660
    22
  val output_width: string -> output * int
wenzelm@23660
    23
  val output: string -> output
wenzelm@23660
    24
  val escape: output -> string
wenzelm@39733
    25
  val raw_stdout: output -> unit
wenzelm@39733
    26
  val raw_stderr: output -> unit
wenzelm@39733
    27
  val raw_writeln: output -> unit
wenzelm@40133
    28
  structure Private_Hooks:
wenzelm@40133
    29
  sig
wenzelm@40133
    30
    val writeln_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    31
    val urgent_message_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    32
    val tracing_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    33
    val warning_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    34
    val error_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    35
    val prompt_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    36
    val status_fn: (output -> unit) Unsynchronized.ref
wenzelm@40133
    37
    val report_fn: (output -> unit) Unsynchronized.ref
wenzelm@43746
    38
    val raw_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
wenzelm@40133
    39
  end
wenzelm@40132
    40
  val urgent_message: string -> unit
wenzelm@25845
    41
  val error_msg: string -> unit
wenzelm@25845
    42
  val prompt: string -> unit
wenzelm@27605
    43
  val status: string -> unit
wenzelm@38236
    44
  val report: string -> unit
wenzelm@43746
    45
  val raw_message: Properties.T -> string -> unit
wenzelm@14815
    46
end;
wenzelm@14815
    47
wenzelm@14815
    48
structure Output: OUTPUT =
wenzelm@14815
    49
struct
wenzelm@14815
    50
wenzelm@23616
    51
(** print modes **)
wenzelm@14881
    52
wenzelm@23660
    53
type output = string;  (*raw system output*)
wenzelm@23660
    54
wenzelm@23616
    55
fun default_output s = (s, size s);
wenzelm@23660
    56
fun default_escape (s: output) = s;
wenzelm@14815
    57
wenzelm@23616
    58
local
wenzelm@23616
    59
  val default = {output = default_output, escape = default_escape};
wenzelm@43684
    60
  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
wenzelm@23616
    61
in
wenzelm@43684
    62
  fun add_mode name output escape =
wenzelm@43684
    63
    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
wenzelm@23616
    64
  fun get_mode () =
wenzelm@43684
    65
    the_default default
wenzelm@43684
    66
      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
wenzelm@23616
    67
end;
wenzelm@14815
    68
wenzelm@19265
    69
fun output_width x = #output (get_mode ()) x;
wenzelm@14815
    70
val output = #1 o output_width;
wenzelm@23727
    71
wenzelm@23616
    72
fun escape x = #escape (get_mode ()) x;
wenzelm@14815
    73
wenzelm@14815
    74
wenzelm@14815
    75
wenzelm@14815
    76
(** output channels **)
wenzelm@14815
    77
wenzelm@39733
    78
(* raw output primitives -- not to be used in user-space *)
wenzelm@14984
    79
wenzelm@39733
    80
fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
wenzelm@39733
    81
fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
wenzelm@14815
    82
wenzelm@39733
    83
fun raw_writeln "" = ()
wenzelm@39733
    84
  | raw_writeln s = raw_stdout (suffix "\n" s);  (*atomic output!*)
wenzelm@14815
    85
wenzelm@14984
    86
wenzelm@14984
    87
(* Isabelle output channels *)
wenzelm@14984
    88
wenzelm@40133
    89
structure Private_Hooks =
wenzelm@40133
    90
struct
wenzelm@40133
    91
  val writeln_fn = Unsynchronized.ref raw_writeln;
wenzelm@40133
    92
  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@40133
    93
  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
wenzelm@40133
    94
  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
wenzelm@40133
    95
  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
wenzelm@40133
    96
  val prompt_fn = Unsynchronized.ref raw_stdout;
wenzelm@43746
    97
  val status_fn = Unsynchronized.ref (fn _: output => ());
wenzelm@43746
    98
  val report_fn = Unsynchronized.ref (fn _: output => ());
wenzelm@43748
    99
  val raw_message_fn =
wenzelm@43748
   100
    Unsynchronized.ref
wenzelm@43748
   101
      (fn _: Properties.T => fn _: output => raise Fail "Output.raw_message undefined");
wenzelm@40133
   102
end;
wenzelm@14815
   103
wenzelm@40133
   104
fun writeln s = ! Private_Hooks.writeln_fn (output s);
wenzelm@40133
   105
fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
wenzelm@40133
   106
fun tracing s = ! Private_Hooks.tracing_fn (output s);
wenzelm@40133
   107
fun warning s = ! Private_Hooks.warning_fn (output s);
wenzelm@40133
   108
fun error_msg s = ! Private_Hooks.error_fn (output s);
wenzelm@40133
   109
fun prompt s = ! Private_Hooks.prompt_fn (output s);
wenzelm@40133
   110
fun status s = ! Private_Hooks.status_fn (output s);
wenzelm@40133
   111
fun report s = ! Private_Hooks.report_fn (output s);
wenzelm@43746
   112
fun raw_message props s = ! Private_Hooks.raw_message_fn props (output s);
aspinall@15190
   113
wenzelm@37784
   114
fun legacy_feature s = warning ("Legacy feature! " ^ s);
wenzelm@22826
   115
wenzelm@14815
   116
end;
wenzelm@14815
   117
wenzelm@32738
   118
structure Basic_Output: BASIC_OUTPUT = Output;
wenzelm@32738
   119
open Basic_Output;