src/Pure/GUI/gui.scala

--- a/src/Pure/GUI/gui.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -80,9 +80,10 @@
 
   /* simple dialogs */
 
-  def scrollable_text(txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
+  def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)
     : ScrollPane =
   {
+    val txt = Output.clean_yxml(raw_txt)
     val text = new TextArea(txt)
     if (width > 0) text.columns = width
     if (height > 0 && split_lines(txt).length > height) text.rows = height