src/Tools/jEdit/src/jedit_editor.scala

--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -128,10 +128,7 @@
   {
     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     if (navigator != null) {
-      try {
-        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
-        m.invoke(null, view)
-      }
+      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
       catch { case _: NoSuchMethodException => }
     }
   }