# HG changeset patch
# User wenzelm
# Date 1460223505 -7200
# Node ID f14569a9ab9324194f6ec9ed3ebc7815f257297b
# Parent  db12de2367ca6416c5853daf5546eb5089bbefb2
proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;

diff -r db12de2367ca -r f14569a9ab93 src/Pure/General/output_primitives.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;
diff -r db12de2367ca -r f14569a9ab93 src/Pure/General/output_primitives_virtual.ML
--- 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;
diff -r db12de2367ca -r f14569a9ab93 src/Pure/PIDE/markup.ML
--- 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 =