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;