--- a/src/Tools/jEdit/src/pretty_text_area.scala Sun Dec 30 16:59:11 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sun Dec 30 18:23:07 2012 +0100
@@ -17,7 +17,7 @@
import org.gjt.sp.jedit.{jEdit, View, Registers}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
import org.gjt.sp.jedit.syntax.SyntaxStyle
-import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.util.{SyntaxUtilities, Log}
object Pretty_Text_Area
@@ -119,7 +119,8 @@
future_rendering = Some(default_thread_pool.submit(() =>
{
val (text, rendering) =
- Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body)
+ try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
+ catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
Simple_Thread.interrupted_exception()
Swing_Thread.later {