# HG changeset patch
# User wenzelm
# Date 1572687791 -3600
# Node ID 64a20b562e6363eb74b4ebe6237f9dbb8854a29f
# Parent  38ade730f6dfdd127e02eafb7eb8a4f2dca47ed4
tuned;

diff -r 38ade730f6df -r 64a20b562e63 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Fri Nov 01 19:40:55 2019 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Nov 02 10:43:11 2019 +0100
@@ -20,12 +20,12 @@
   val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
-  val output_markup: Markup.T -> string * string
   val buffer_body: XML.body -> Buffer.T -> Buffer.T
   val buffer: XML.tree -> Buffer.T -> Buffer.T
   val chunks_of_body: XML.body -> string list
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
+  val output_markup: Markup.T -> string * string
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
@@ -65,10 +65,6 @@
 
 (* output *)
 
-fun output_markup (markup as (name, atts)) =
-  if Markup.is_empty markup then Markup.no_output
-  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-
 fun buffer_attrib (a, x) =
   Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
 
@@ -84,11 +80,15 @@
 val string_of = string_of_body o single;
 
 
-(* wrapped elements *)
+(* markup elements *)
 
 val Z = chr 0;
 val Z_text = [XML.Text Z];
 
+fun output_markup (markup as (name, atts)) =
+  if Markup.is_empty markup then Markup.no_output
+  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;