# HG changeset patch
# User wenzelm
# Date 1543176655 -3600
# Node ID 6bd63c94cf62e7293e50e4f2fdc6c2593de77faf
# Parent  f87fdd8d2bafbfd176f70f26f851bb6aae8222f8
tuned signature (see also src/Tools/Haskell/Markup.hs);

diff -r f87fdd8d2baf -r 6bd63c94cf62 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Nov 25 18:45:10 2018 +0100
+++ b/src/Pure/General/pretty.ML	Sun Nov 25 21:10:55 2018 +0100
@@ -23,7 +23,7 @@
   val default_indent: string -> int -> Output.output
   val add_mode: string -> (string -> int -> Output.output) -> unit
   type T
-  val make_block: {markup: Output.output * Output.output, consistent: bool, indent: int} ->
+  val make_block: {markup: Markup.output, consistent: bool, indent: int} ->
     T list -> T
   val markup_block: {markup: Markup.T, consistent: bool, indent: int} -> T list -> T
   val str: string -> T
@@ -113,7 +113,7 @@
 val force_nat = Integer.max 0;
 
 abstype T =
-    Block of (Output.output * Output.output) * bool * int * T list * int
+    Block of Markup.output * bool * int * T list * int
       (*markup output, consistent, indentation, body, length*)
   | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
   | Str of Output.output * int  (*text, length*)
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
diff -r f87fdd8d2baf -r 6bd63c94cf62 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Sun Nov 25 18:45:10 2018 +0100
+++ b/src/Pure/PIDE/xml.ML	Sun Nov 25 21:10:55 2018 +0100
@@ -44,7 +44,7 @@
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
-  val output_markup: Markup.T -> Output.output * Output.output
+  val output_markup: Markup.T -> Markup.output
   val string_of: tree -> string
   val pretty: int -> tree -> Pretty.T
   val output: tree -> BinIO.outstream -> unit