src/Tools/jEdit/src/rich_text_area.scala

       else {
         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
         default
       }
     }
-    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
   }
 
 
   /* original painters */