src/Pure/General/output_primitives_virtual.ML
author wenzelm
Wed, 20 Mar 2019 23:06:51 +0100
changeset 69933 c15ee153dec1
parent 62978 c04eead96cca
permissions -rw-r--r--
updated to cygwin-20190320;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62978
c04eead96cca tuned headers;
wenzelm
parents: 62933
diff changeset
     1
(*  Title:      Pure/General/output_primitives_virtual.ML
62930
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 -- virtual version within Pure environment.
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
structure Output_Primitives_Virtual: OUTPUT_PRIMITIVES =
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     8
struct
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
     9
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    10
open Output_Primitives;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    11
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    12
fun writeln_fn x = ! Private_Output.writeln_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    13
fun state_fn x = ! Private_Output.state_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    14
fun information_fn x = ! Private_Output.information_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    15
fun tracing_fn x = ! Private_Output.tracing_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    16
fun warning_fn x = ! Private_Output.warning_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    17
fun legacy_fn x = ! Private_Output.legacy_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    18
fun error_message_fn x = ! Private_Output.error_message_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    19
fun system_message_fn x = ! Private_Output.system_message_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    20
fun status_fn x = ! Private_Output.status_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    21
fun report_fn x = ! Private_Output.report_fn x;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    22
fun result_fn x y = ! Private_Output.result_fn x y;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    23
fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y;
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    24
62933
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
wenzelm
parents: 62930
diff changeset
    25
val markup_fn = Markup.output;
f14569a9ab93 proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
wenzelm
parents: 62930
diff changeset
    26
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents:
diff changeset
    27
end;