# HG changeset patch
# User wenzelm
# Date 1356888187 -3600
# Node ID b35bd877875430f1aea4bcf170d38ce2448c5d05
# Parent  f1c2f911ae33b3ee7d8b12063c434ca5ff20a1a4
more informative error;

diff -r f1c2f911ae33 -r b35bd8778754 src/Tools/jEdit/src/pretty_text_area.scala
--- 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 {