--- a/src/Pure/PIDE/yxml.ML Sat Sep 29 13:43:23 2012 +0200
+++ b/src/Pure/PIDE/yxml.ML Sat Sep 29 16:15:18 2012 +0200
@@ -23,6 +23,7 @@
val output_markup: Markup.T -> string * string
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
+ val output_markup_elem: Markup.T -> (string * string) * string
val parse_body: string -> XML.body
val parse: string -> XML.tree
end;
@@ -75,6 +76,16 @@
val string_of = string_of_body o single;
+(* wrapped elements *)
+
+val Z = chr 0;
+val Z_text = [XML.Text Z];
+
+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;
+
+
(** efficient YXML parsing **)