src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
author immler@in.tum.de
Fri May 22 14:47:57 2009 +0200 (2009-05-22)
changeset 34568 b517d0607297
child 34569 15abc5f5f40a
permissions -rw-r--r--
implemented IsabelleHyperlinkSource (only links inside the current buffer)
immler@34568
     1
/*
immler@34568
     2
 * IsabelleHyperlinkSource.scala
immler@34568
     3
 *
immler@34568
     4
 * To change this template, choose Tools | Template Manager
immler@34568
     5
 * and open the template in the editor.
immler@34568
     6
 */
immler@34568
     7
immler@34568
     8
package isabelle.jedit
immler@34568
     9
import gatchan.jedit.hyperlinks.Hyperlink
immler@34568
    10
import gatchan.jedit.hyperlinks.HyperlinkSource
immler@34568
    11
import gatchan.jedit.hyperlinks.AbstractHyperlink
immler@34568
    12
immler@34568
    13
import org.gjt.sp.jedit.View
immler@34568
    14
import org.gjt.sp.jedit.jEdit
immler@34568
    15
import org.gjt.sp.jedit.Buffer
immler@34568
    16
import org.gjt.sp.jedit.TextUtilities
immler@34568
    17
immler@34568
    18
import isabelle.prover.RefInfo
immler@34568
    19
immler@34568
    20
class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
immler@34568
    21
  extends AbstractHyperlink(start, end, line, "tooltip")
immler@34568
    22
{
immler@34568
    23
  override def click(view: View) = {
immler@34568
    24
    view.getTextArea.moveCaretPosition(ref_offset)
immler@34568
    25
  }
immler@34568
    26
}
immler@34568
    27
immler@34568
    28
class IsabelleHyperlinkSource extends HyperlinkSource
immler@34568
    29
{
immler@34568
    30
	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
immler@34568
    31
    val prover = Isabelle.prover_setup(buffer).map(_.prover)
immler@34568
    32
    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
immler@34568
    33
    if (!prover.isDefined || !theory_view_opt.isDefined) null
immler@34568
    34
    else if (prover.get == null || theory_view_opt.get == null) null
immler@34568
    35
    else {
immler@34568
    36
      val document = prover.get.document
immler@34568
    37
      val theory_view = theory_view_opt.get
immler@34568
    38
      val offset = theory_view.from_current(document, original_offset)
immler@34568
    39
      val cmd = document.find_command_at(offset)
immler@34568
    40
      if (cmd != null) {
immler@34568
    41
        val ref_o = cmd.ref_at(offset - cmd.start(document))
immler@34568
    42
        if (!ref_o.isDefined) null
immler@34568
    43
        else {
immler@34568
    44
          val ref = ref_o.get
immler@34568
    45
          val start = theory_view.to_current(document, ref.abs_start(document))
immler@34568
    46
          val line = buffer.getLineOfOffset(start)
immler@34568
    47
          val end = theory_view.to_current(document, ref.abs_stop(document))
immler@34568
    48
          ref.info match {
immler@34568
    49
            case RefInfo(Some(file), Some(ref_line), _, _) =>
immler@34568
    50
              null
immler@34568
    51
            case RefInfo(_, _, Some(id), Some(offset)) =>
immler@34568
    52
              prover.get.command(id) match {
immler@34568
    53
                case Some(ref_cmd) =>
immler@34568
    54
                  new InternalHyperlink(start, end, line,
immler@34568
    55
                    theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
immler@34568
    56
                case _ => null
immler@34568
    57
              }
immler@34568
    58
            case _ => null
immler@34568
    59
          }
immler@34568
    60
        }
immler@34568
    61
      } else null
immler@34568
    62
    }
immler@34568
    63
  }
immler@34568
    64
}