proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
authorwenzelm
Sat, 09 Apr 2016 19:38:25 +0200
changeset 62933 f14569a9ab93
parent 62932 db12de2367ca
child 62934 6e3fb0aa857a
proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML;
src/Pure/General/output_primitives.ML
src/Pure/General/output_primitives_virtual.ML
src/Pure/PIDE/markup.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 =