src/Tools/jEdit/src/jedit_editor.scala
changeset 58545 30b75b7958d6
parent 57878 51a2f9140175
child 59080 611914621edb
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 16:05:17 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Oct 05 17:58:36 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  import java.io.{File => JFile}
     1.6  
     1.7 -import org.gjt.sp.jedit.{jEdit, View}
     1.8 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
     1.9  import org.gjt.sp.jedit.browser.VFSBrowser
    1.10  
    1.11  
    1.12 @@ -136,6 +136,20 @@
    1.13      }
    1.14    }
    1.15  
    1.16 +  def goto_buffer(view: View, buffer: Buffer, offset: Text.Offset)
    1.17 +  {
    1.18 +    GUI_Thread.require {}
    1.19 +
    1.20 +    push_position(view)
    1.21 +
    1.22 +    view.goToBuffer(buffer)
    1.23 +    try { view.getTextArea.moveCaretPosition(offset) }
    1.24 +    catch {
    1.25 +      case _: ArrayIndexOutOfBoundsException =>
    1.26 +      case _: IllegalArgumentException =>
    1.27 +    }
    1.28 +  }
    1.29 +
    1.30    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    1.31    {
    1.32      GUI_Thread.require {}
    1.33 @@ -186,6 +200,13 @@
    1.34        override def toString: String = "URL " + quote(name)
    1.35      }
    1.36  
    1.37 +  def hyperlink_buffer(buffer: Buffer, offset: Text.Offset): Hyperlink =
    1.38 +    new Hyperlink {
    1.39 +      val external = false
    1.40 +      def follow(view: View): Unit = goto_buffer(view, buffer, offset)
    1.41 +      override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer))
    1.42 +    }
    1.43 +
    1.44    def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
    1.45      new Hyperlink {
    1.46        val external = false