| author | paulson <lp15@cam.ac.uk> |
| Fri, 08 Aug 2025 16:46:03 +0100 | |
| changeset 82969 | dedd9d13c79c |
| parent 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; |
|
|
82316
83584916b6d7
support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);
wenzelm
parents:
62978
diff
changeset
|
13 |
fun writeln_urgent_fn x = ! Private_Output.writeln_urgent_fn x; |
| 62930 | 14 |
fun state_fn x = ! Private_Output.state_fn x; |
15 |
fun information_fn x = ! Private_Output.information_fn x; |
|
16 |
fun tracing_fn x = ! Private_Output.tracing_fn x; |
|
17 |
fun warning_fn x = ! Private_Output.warning_fn x; |
|
18 |
fun legacy_fn x = ! Private_Output.legacy_fn x; |
|
19 |
fun error_message_fn x = ! Private_Output.error_message_fn x; |
|
20 |
fun system_message_fn x = ! Private_Output.system_message_fn x; |
|
21 |
fun status_fn x = ! Private_Output.status_fn x; |
|
22 |
fun report_fn x = ! Private_Output.report_fn x; |
|
23 |
fun result_fn x y = ! Private_Output.result_fn x y; |
|
24 |
fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y; |
|
25 |
||
|
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 = 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
|
27 |
|
| 62930 | 28 |
end; |