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