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