changeset 50216 | de77cde57376 |
parent 50205 | 788c8263e634 |
child 50306 | b655d2d0406d |
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Nov 26 16:16:47 2012 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Nov 26 16:22:29 2012 +0100 @@ -93,6 +93,7 @@ Swing_Thread.later { current_rendering = rendering JEdit_Lib.buffer_edit(getBuffer) { + rich_text_area.active_reset() getBuffer.setReadOnly(false) setText(text) setCaretPosition(0)