tuned;
authorwenzelm
Sun Dec 30 18:23:31 2012 +0100 (2012-12-30)
changeset 50641b908e56e83ca
parent 50640 b35bd8778754
child 50642 aca12f646772
tuned;
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/Thy/thy_load.scala	Sun Dec 30 18:23:07 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.scala	Sun Dec 30 18:23:31 2012 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4        val uses = header.uses
     1.5        Document.Node.Header(imports, header.keywords, uses)
     1.6      }
     1.7 -    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
     1.8 +    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     1.9    }
    1.10  
    1.11    def check_thy(name: Document.Node.Name): Document.Node.Header =
     2.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 30 18:23:07 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Dec 30 18:23:31 2012 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4          default
     2.5        }
     2.6      }
     2.7 -    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
     2.8 +    catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); default }
     2.9    }
    2.10  
    2.11