src/Tools/jEdit/src/jedit_editor.scala
changeset 56413 2d4d9a5f68ff
parent 56373 0605d90be6fc
child 56457 eea4bbe15745
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 22:21:46 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Fri Apr 04 22:51:22 2014 +0200
     1.3 @@ -111,10 +111,24 @@
     1.4  
     1.5    /* navigation */
     1.6  
     1.7 +  def push_position(view: View)
     1.8 +  {
     1.9 +    val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
    1.10 +    if (navigator != null) {
    1.11 +      try {
    1.12 +        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
    1.13 +        m.invoke(null, view)
    1.14 +      }
    1.15 +      catch { case _: NoSuchMethodException => }
    1.16 +    }
    1.17 +  }
    1.18 +
    1.19    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    1.20    {
    1.21      Swing_Thread.require()
    1.22  
    1.23 +    push_position(view)
    1.24 +
    1.25      JEdit_Lib.jedit_buffer(name) match {
    1.26        case Some(buffer) =>
    1.27          view.goToBuffer(buffer)