src/Pure/General/output_primitives.ML
author wenzelm
Sat Apr 09 16:16:05 2016 +0200 (2016-04-09)
changeset 62930 51ac6bc389e8
child 62933 f14569a9ab93
permissions -rw-r--r--
shared output primitives of physical/virtual Pure;
wenzelm@62930
     1
(*  Title:      Pure/General/output_primitives.ML
wenzelm@62930
     2
    Author:     Makarius
wenzelm@62930
     3
wenzelm@62930
     4
Primitives for Isabelle output channels.
wenzelm@62930
     5
*)
wenzelm@62930
     6
wenzelm@62930
     7
signature OUTPUT_PRIMITIVES =
wenzelm@62930
     8
sig
wenzelm@62930
     9
  type output = string
wenzelm@62930
    10
  type serial = int
wenzelm@62930
    11
  type properties = (string * string) list
wenzelm@62930
    12
  val writeln_fn: output list -> unit
wenzelm@62930
    13
  val state_fn: output list -> unit
wenzelm@62930
    14
  val information_fn: output list -> unit
wenzelm@62930
    15
  val tracing_fn: output list -> unit
wenzelm@62930
    16
  val warning_fn: output list -> unit
wenzelm@62930
    17
  val legacy_fn: output list -> unit
wenzelm@62930
    18
  val error_message_fn: serial * output list -> unit
wenzelm@62930
    19
  val system_message_fn: output list -> unit
wenzelm@62930
    20
  val status_fn: output list -> unit
wenzelm@62930
    21
  val report_fn: output list -> unit
wenzelm@62930
    22
  val result_fn: properties -> output list -> unit
wenzelm@62930
    23
  val protocol_message_fn: properties -> output list -> unit
wenzelm@62930
    24
end;
wenzelm@62930
    25
wenzelm@62930
    26
structure Output_Primitives: OUTPUT_PRIMITIVES =
wenzelm@62930
    27
struct
wenzelm@62930
    28
wenzelm@62930
    29
type output = string;
wenzelm@62930
    30
type serial = int;
wenzelm@62930
    31
type properties = (string * string) list;
wenzelm@62930
    32
wenzelm@62930
    33
fun ignore_outputs (_: output list) = ();
wenzelm@62930
    34
wenzelm@62930
    35
val writeln_fn = ignore_outputs;
wenzelm@62930
    36
val state_fn = ignore_outputs;
wenzelm@62930
    37
val information_fn = ignore_outputs;
wenzelm@62930
    38
val tracing_fn = ignore_outputs;
wenzelm@62930
    39
val warning_fn = ignore_outputs;
wenzelm@62930
    40
val legacy_fn = ignore_outputs;
wenzelm@62930
    41
fun error_message_fn (_: serial, _: output list) = ();
wenzelm@62930
    42
val system_message_fn = ignore_outputs;
wenzelm@62930
    43
val status_fn = ignore_outputs;
wenzelm@62930
    44
val report_fn = ignore_outputs;
wenzelm@62930
    45
fun result_fn (_: properties) = ignore_outputs;
wenzelm@62930
    46
fun protocol_message_fn (_: properties) = ignore_outputs;
wenzelm@62930
    47
wenzelm@62930
    48
end;