equal
deleted
inserted
replaced
90 val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) |
90 val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) |
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 |
95 JEdit_Lib.buffer_edit(getBuffer) { |
96 try { |
|
97 getBuffer.beginCompoundEdit |
|
98 getBuffer.setReadOnly(false) |
96 getBuffer.setReadOnly(false) |
99 setText(text) |
97 setText(text) |
100 setCaretPosition(0) |
98 setCaretPosition(0) |
101 getBuffer.setReadOnly(true) |
99 getBuffer.setReadOnly(true) |
102 } |
|
103 finally { |
|
104 getBuffer.endCompoundEdit |
|
105 } |
100 } |
106 } |
101 } |
107 })) |
102 })) |
108 } |
103 } |
109 } |
104 } |