--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 22:21:46 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Apr 04 22:51:22 2014 +0200
@@ -111,10 +111,24 @@
/* navigation */
+ def push_position(view: View)
+ {
+ val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
+ if (navigator != null) {
+ try {
+ val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
+ m.invoke(null, view)
+ }
+ catch { case _: NoSuchMethodException => }
+ }
+ }
+
def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
{
Swing_Thread.require()
+ push_position(view)
+
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
view.goToBuffer(buffer)