--- 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*)
--- 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
--- 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