| author | blanchet |
| Tue, 19 Dec 2017 14:51:27 +0100 | |
| changeset 67225 | cb34f5f49a08 |
| parent 62978 | c04eead96cca |
| child 82316 | 83584916b6d7 |
| permissions | -rw-r--r-- |
| 62978 | 1 |
(* Title: Pure/General/output_primitives_virtual.ML |
| 62930 | 2 |
Author: Makarius |
3 |
||
4 |
Primitives for Isabelle output channels -- virtual version within Pure environment. |
|
5 |
*) |
|
6 |
||
7 |
structure Output_Primitives_Virtual: OUTPUT_PRIMITIVES = |
|
8 |
struct |
|
9 |
||
10 |
open Output_Primitives; |
|
11 |
||
12 |
fun writeln_fn x = ! Private_Output.writeln_fn x; |
|
13 |
fun state_fn x = ! Private_Output.state_fn x; |
|
14 |
fun information_fn x = ! Private_Output.information_fn x; |
|
15 |
fun tracing_fn x = ! Private_Output.tracing_fn x; |
|
16 |
fun warning_fn x = ! Private_Output.warning_fn x; |
|
17 |
fun legacy_fn x = ! Private_Output.legacy_fn x; |
|
18 |
fun error_message_fn x = ! Private_Output.error_message_fn x; |
|
19 |
fun system_message_fn x = ! Private_Output.system_message_fn x; |
|
20 |
fun status_fn x = ! Private_Output.status_fn x; |
|
21 |
fun report_fn x = ! Private_Output.report_fn x; |
|
22 |
fun result_fn x y = ! Private_Output.result_fn x y; |
|
23 |
fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y; |
|
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 | 27 |
end; |