equal
deleted
inserted
replaced
91 Simple_Thread.interrupted_exception() |
91 Simple_Thread.interrupted_exception() |
92 |
92 |
93 Swing_Thread.later { |
93 Swing_Thread.later { |
94 current_rendering = rendering |
94 current_rendering = rendering |
95 JEdit_Lib.buffer_edit(getBuffer) { |
95 JEdit_Lib.buffer_edit(getBuffer) { |
|
96 rich_text_area.active_reset() |
96 getBuffer.setReadOnly(false) |
97 getBuffer.setReadOnly(false) |
97 setText(text) |
98 setText(text) |
98 setCaretPosition(0) |
99 setCaretPosition(0) |
99 getBuffer.setReadOnly(true) |
100 getBuffer.setReadOnly(true) |
100 } |
101 } |