src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Thu Sep 20 10:43:04 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Sep 20 11:09:53 2012 +0200
@@ -112,7 +112,8 @@
 
   def rich_text(id: Document.Command_ID, body: XML.Body): Command =
   {
-    val (text, markup) = XML.content_markup(body)
+    val text = XML.content(body)
+    val markup = Markup_Tree.from_XML(body)
     unparsed(id, text, markup)
   }