src/Tools/jEdit/src/jedit_editor.scala
changeset 59080 611914621edb
parent 58545 30b75b7958d6
child 59319 677615cba30d
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 16:40:11 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 17:30:53 2014 +0100
     1.3 @@ -128,10 +128,7 @@
     1.4    {
     1.5      val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     1.6      if (navigator != null) {
     1.7 -      try {
     1.8 -        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
     1.9 -        m.invoke(null, view)
    1.10 -      }
    1.11 +      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
    1.12        catch { case _: NoSuchMethodException => }
    1.13      }
    1.14    }