src/Pure/General/output_primitives.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output_primitives.ML	Sat Apr 09 16:16:05 2016 +0200
@@ -0,0 +1,48 @@
+(*  Title:      Pure/General/output_primitives.ML
+    Author:     Makarius
+
+Primitives for Isabelle output channels.
+*)
+
+signature OUTPUT_PRIMITIVES =
+sig
+  type output = string
+  type serial = int
+  type properties = (string * string) list
+  val writeln_fn: output list -> unit
+  val state_fn: output list -> unit
+  val information_fn: output list -> unit
+  val tracing_fn: output list -> unit
+  val warning_fn: output list -> unit
+  val legacy_fn: output list -> unit
+  val error_message_fn: serial * output list -> unit
+  val system_message_fn: output list -> unit
+  val status_fn: output list -> unit
+  val report_fn: output list -> unit
+  val result_fn: properties -> output list -> unit
+  val protocol_message_fn: properties -> output list -> unit
+end;
+
+structure Output_Primitives: OUTPUT_PRIMITIVES =
+struct
+
+type output = string;
+type serial = int;
+type properties = (string * string) list;
+
+fun ignore_outputs (_: output list) = ();
+
+val writeln_fn = ignore_outputs;
+val state_fn = ignore_outputs;
+val information_fn = ignore_outputs;
+val tracing_fn = ignore_outputs;
+val warning_fn = ignore_outputs;
+val legacy_fn = ignore_outputs;
+fun error_message_fn (_: serial, _: output list) = ();
+val system_message_fn = ignore_outputs;
+val status_fn = ignore_outputs;
+val report_fn = ignore_outputs;
+fun result_fn (_: properties) = ignore_outputs;
+fun protocol_message_fn (_: properties) = ignore_outputs;
+
+end;