diff -r f87fdd8d2baf -r 6bd63c94cf62 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sun Nov 25 18:45:10 2018 +0100
+++ b/src/Pure/PIDE/markup.ML	Sun Nov 25 21:10:55 2018 +0100
@@ -225,9 +225,10 @@
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
-  val no_output: Output.output * Output.output
-  val add_mode: string -> (T -> Output.output * Output.output) -> unit
-  val output: T -> Output.output * Output.output
+  type output = Output.output * Output.output
+  val no_output: output
+  val add_mode: string -> (T -> output) -> unit
+  val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
@@ -697,6 +698,8 @@
 
 (** print mode operations **)
 
+type output = Output.output * Output.output;
+
 val no_output = ("", "");
 
 local