src/Pure/General/output_primitives.ML
author wenzelm
Mon, 02 Sep 2024 15:23:12 +0200
changeset 80801 090adcdceaae
parent 73559 22b5ecb53dd9
permissions -rw-r--r--
clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/output_primitives.ML
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     3
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     4
Primitives for Isabelle output channels.
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     5
*)
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     6
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     7
signature OUTPUT_PRIMITIVES =
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     8
sig
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     9
  type output = string
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    10
  type serial = int
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    11
  type properties = (string * string) list
65301
fca593a62785 restore output channels after shutdown, e.g. relevant for saved heap;
wenzelm
parents: 62933
diff changeset
    12
  val ignore_outputs: output list -> unit
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    13
  val writeln_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    14
  val state_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    15
  val information_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    16
  val tracing_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    17
  val warning_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    18
  val legacy_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    19
  val error_message_fn: serial * output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    20
  val system_message_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    21
  val status_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    22
  val report_fn: output list -> unit
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    23
  val result_fn: properties -> output list -> unit
73559
22b5ecb53dd9 more uniform use of Byte_Message;
wenzelm
parents: 71617
diff changeset
    24
  type protocol_message_fn = properties -> XML.body list -> unit
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 65301
diff changeset
    25
  val protocol_message_fn: protocol_message_fn
62933
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
wenzelm
parents: 62930
diff changeset
    26
  val markup_fn: string * properties -> output * output
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    27
end;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    28
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    29
structure Output_Primitives: OUTPUT_PRIMITIVES =
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    30
struct
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    31
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 65301
diff changeset
    32
(* output *)
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 65301
diff changeset
    33
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    34
type output = string;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    35
type serial = int;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    36
type properties = (string * string) list;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    37
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    38
fun ignore_outputs (_: output list) = ();
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    39
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    40
val writeln_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    41
val state_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    42
val information_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    43
val tracing_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    44
val warning_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    45
val legacy_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    46
fun error_message_fn (_: serial, _: output list) = ();
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    47
val system_message_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    48
val status_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    49
val report_fn = ignore_outputs;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    50
fun result_fn (_: properties) = ignore_outputs;
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 65301
diff changeset
    51
73559
22b5ecb53dd9 more uniform use of Byte_Message;
wenzelm
parents: 71617
diff changeset
    52
type protocol_message_fn = properties -> XML.body list -> unit;
70991
f9f7c34b7dd4 more scalable protocol_message: use XML.body directly (Output.output hook is not required);
wenzelm
parents: 65301
diff changeset
    53
val protocol_message_fn: protocol_message_fn = fn _ => fn _ => ();
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    54
62933
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
wenzelm
parents: 62930
diff changeset
    55
fun markup_fn (_: string * properties) = ("", "");
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
wenzelm
parents: 62930
diff changeset
    56
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    57
end;