# 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 {