src/Tools/jEdit/src/hyperlink.scala

tuned signature;

/*  Title:      Tools/jEdit/src/hyperlink.scala
    Author:     Fabian Immler, TU Munich
    Author:     Makarius

Hyperlinks within jEdit buffers for PIDE proof documents.
*/

package isabelle.jedit


import isabelle._

import org.gjt.sp.jedit.{View, jEdit}
import org.gjt.sp.jedit.textarea.JEditTextArea


object Hyperlink
{
  def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink =
    File_Link(jedit_file, line, column)
}

abstract class Hyperlink
{
  def follow(view: View): Unit
}

private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink
{
  override def follow(view: View)
  {
    Swing_Thread.require()

    JEdit_Lib.jedit_buffer(jedit_file) match {
      case Some(buffer) =>
        view.goToBuffer(buffer)
        val text_area = view.getTextArea

        try {
          val line_start = text_area.getBuffer.getLineStartOffset(line - 1)
          text_area.moveCaretPosition(line_start)
          if (column > 0) text_area.moveCaretPosition(line_start + column - 1)
        }
        catch {
          case _: ArrayIndexOutOfBoundsException =>
          case _: IllegalArgumentException =>
        }

      case None =>
        val args =
          if (line <= 0) Array(jedit_file)
          else if (column <= 0) Array(jedit_file, "+line:" + line.toInt)
          else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt)
        jEdit.openFiles(view, null, args)
    }
  }
}