src/Tools/jEdit/src/output_dockable.scala
changeset 49411 1da54e9bda68
parent 49410 34acbcc33adf
child 49414 d7b5fb2e9ca2
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 17 20:23:25 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 17 20:34:19 2012 +0200
@@ -47,7 +47,7 @@
         val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
         Document_View(view.getTextArea) match {
           case Some(doc_view) =>
-            doc_view.text_area_painter.robust_body() {
+            doc_view.rich_text_area.robust_body() {
               val cmd = current_state.command
               val model = doc_view.model
               val buffer = model.buffer