# HG changeset patch
# User wenzelm
# Date 1356888211 -3600
# Node ID b908e56e83ca1ea7e90fa0137e0dd84c7a6ac0ec
# Parent  b35bd877875430f1aea4bcf170d38ce2448c5d05
tuned;

diff -r b35bd8778754 -r b908e56e83ca src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Sun Dec 30 18:23:07 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Sun Dec 30 18:23:31 2012 +0100
@@ -117,7 +117,7 @@
       val uses = header.uses
       Document.Node.Header(imports, header.keywords, uses)
     }
-    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
+    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   }
 
   def check_thy(name: Document.Node.Name): Document.Node.Header =
diff -r b35bd8778754 -r b908e56e83ca src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 30 18:23:07 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 30 18:23:31 2012 +0100
@@ -45,7 +45,7 @@
         default
       }
     }
-    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
   }