proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
--- a/src/Pure/General/output_primitives.ML Sat Apr 09 19:30:15 2016 +0200
+++ b/src/Pure/General/output_primitives.ML Sat Apr 09 19:38:25 2016 +0200
@@ -21,6 +21,7 @@
val report_fn: output list -> unit
val result_fn: properties -> output list -> unit
val protocol_message_fn: properties -> output list -> unit
+ val markup_fn: string * properties -> output * output
end;
structure Output_Primitives: OUTPUT_PRIMITIVES =
@@ -45,4 +46,6 @@
fun result_fn (_: properties) = ignore_outputs;
fun protocol_message_fn (_: properties) = ignore_outputs;
+fun markup_fn (_: string * properties) = ("", "");
+
end;
--- a/src/Pure/General/output_primitives_virtual.ML Sat Apr 09 19:30:15 2016 +0200
+++ b/src/Pure/General/output_primitives_virtual.ML Sat Apr 09 19:38:25 2016 +0200
@@ -22,4 +22,6 @@
fun result_fn x y = ! Private_Output.result_fn x y;
fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y;
+val markup_fn = Markup.output;
+
end;
--- a/src/Pure/PIDE/markup.ML Sat Apr 09 19:30:15 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Sat Apr 09 19:38:25 2016 +0200
@@ -212,7 +212,6 @@
val simp_trace_ignoreN: string
val simp_trace_cancel: serial -> Properties.T
val no_output: Output.output * Output.output
- val default_output: T -> Output.output * Output.output
val add_mode: string -> (T -> Output.output * Output.output) -> unit
val output: T -> Output.output * Output.output
val enclose: T -> Output.output -> Output.output
@@ -683,10 +682,9 @@
(** print mode operations **)
val no_output = ("", "");
-fun default_output (_: T) = no_output;
local
- val default = {output = default_output};
+ val default = {output = Output_Primitives.markup_fn};
val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
in
fun add_mode name output =