src/Pure/PIDE/yxml.ML
changeset 59433 9da5b2c61049
parent 49656 7ff712de5747
child 64275 ac2abc987cf9
--- a/src/Pure/PIDE/yxml.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -26,6 +26,7 @@
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
+  val content_of: string -> string
 end;
 
 structure YXML: YXML =
@@ -148,5 +149,7 @@
 
 end;
 
+val content_of = parse_body #> XML.content_of;
+
 end;