src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 18 14:51:12 2012 +0200
@@ -109,8 +109,7 @@
 
   def rich_text(id: Document.Command_ID, body: XML.Body): Command =
   {
-    val text = XML.content(body).mkString
-    val markup = Markup_Tree.empty  // FIXME
+    val (text, markup) = XML.content_markup(body)
     unparsed(id, text, markup)
   }