equal
deleted
inserted
replaced
15 import javax.swing.{KeyStroke, JComponent} |
15 import javax.swing.{KeyStroke, JComponent} |
16 |
16 |
17 import org.gjt.sp.jedit.{jEdit, View, Registers} |
17 import org.gjt.sp.jedit.{jEdit, View, Registers} |
18 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} |
18 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} |
19 import org.gjt.sp.jedit.syntax.SyntaxStyle |
19 import org.gjt.sp.jedit.syntax.SyntaxStyle |
20 import org.gjt.sp.util.SyntaxUtilities |
20 import org.gjt.sp.util.{SyntaxUtilities, Log} |
21 |
21 |
22 |
22 |
23 object Pretty_Text_Area |
23 object Pretty_Text_Area |
24 { |
24 { |
25 private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results, |
25 private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results, |
117 |
117 |
118 future_rendering.map(_.cancel(true)) |
118 future_rendering.map(_.cancel(true)) |
119 future_rendering = Some(default_thread_pool.submit(() => |
119 future_rendering = Some(default_thread_pool.submit(() => |
120 { |
120 { |
121 val (text, rendering) = |
121 val (text, rendering) = |
122 Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) |
122 try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) } |
|
123 catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn } |
123 Simple_Thread.interrupted_exception() |
124 Simple_Thread.interrupted_exception() |
124 |
125 |
125 Swing_Thread.later { |
126 Swing_Thread.later { |
126 current_rendering = rendering |
127 current_rendering = rendering |
127 JEdit_Lib.buffer_edit(getBuffer) { |
128 JEdit_Lib.buffer_edit(getBuffer) { |