src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
author immler@in.tum.de
Fri May 22 16:47:11 2009 +0200 (2009-05-22)
changeset 34569 15abc5f5f40a
parent 34568 b517d0607297
child 34573 daa397b6401c
permissions -rw-r--r--
implemented links to other files
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@34569
     9
immler@34569
    10
import java.io.File
immler@34569
    11
immler@34568
    12
import gatchan.jedit.hyperlinks.Hyperlink
immler@34568
    13
import gatchan.jedit.hyperlinks.HyperlinkSource
immler@34568
    14
import gatchan.jedit.hyperlinks.AbstractHyperlink
immler@34568
    15
immler@34568
    16
import org.gjt.sp.jedit.View
immler@34568
    17
import org.gjt.sp.jedit.jEdit
immler@34568
    18
import org.gjt.sp.jedit.Buffer
immler@34568
    19
import org.gjt.sp.jedit.TextUtilities
immler@34568
    20
immler@34568
    21
import isabelle.prover.RefInfo
immler@34568
    22
immler@34568
    23
class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
immler@34569
    24
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    25
{
immler@34568
    26
  override def click(view: View) = {
immler@34568
    27
    view.getTextArea.moveCaretPosition(ref_offset)
immler@34568
    28
  }
immler@34568
    29
}
immler@34568
    30
immler@34569
    31
class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
immler@34569
    32
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    33
{
immler@34569
    34
  val srcs = List(new File(Isabelle.system.getenv("ISABELLE_HOME"), "src"),
immler@34569
    35
                  new File(Isabelle.system.getenv("ML_SOURCES")))
immler@34569
    36
immler@34569
    37
  def find_file(file: File, filename: String): Option[File] =
immler@34569
    38
  {
immler@34569
    39
    if (file.getName == new File(filename).getName) Some(file)
immler@34569
    40
    else if (file.isDirectory) file.listFiles.map(find_file(_, filename)).find(_.isDefined).getOrElse(None)
immler@34569
    41
    else None
immler@34569
    42
  }
immler@34569
    43
immler@34569
    44
  override def click(view: View) = {
immler@34569
    45
    srcs.find(src =>
immler@34569
    46
      find_file(src, ref_file) match {
immler@34569
    47
        case None => false
immler@34569
    48
        case Some(file) =>
immler@34569
    49
          jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
immler@34569
    50
          true})
immler@34569
    51
      match {
immler@34569
    52
        case None => System.err.println("Could not find file " + ref_file)
immler@34569
    53
        case _ =>
immler@34569
    54
      }
immler@34569
    55
  }
immler@34569
    56
}
immler@34569
    57
immler@34568
    58
class IsabelleHyperlinkSource extends HyperlinkSource
immler@34568
    59
{
immler@34568
    60
	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
immler@34568
    61
    val prover = Isabelle.prover_setup(buffer).map(_.prover)
immler@34568
    62
    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
immler@34568
    63
    if (!prover.isDefined || !theory_view_opt.isDefined) null
immler@34568
    64
    else if (prover.get == null || theory_view_opt.get == null) null
immler@34568
    65
    else {
immler@34568
    66
      val document = prover.get.document
immler@34568
    67
      val theory_view = theory_view_opt.get
immler@34568
    68
      val offset = theory_view.from_current(document, original_offset)
immler@34568
    69
      val cmd = document.find_command_at(offset)
immler@34568
    70
      if (cmd != null) {
immler@34568
    71
        val ref_o = cmd.ref_at(offset - cmd.start(document))
immler@34568
    72
        if (!ref_o.isDefined) null
immler@34568
    73
        else {
immler@34568
    74
          val ref = ref_o.get
immler@34568
    75
          val start = theory_view.to_current(document, ref.abs_start(document))
immler@34568
    76
          val line = buffer.getLineOfOffset(start)
immler@34568
    77
          val end = theory_view.to_current(document, ref.abs_stop(document))
immler@34568
    78
          ref.info match {
immler@34569
    79
            case RefInfo(Some(ref_file), Some(ref_line), _, _) =>
immler@34569
    80
              new ExternalHyperlink(start, end, line, ref_file, ref_line)
immler@34568
    81
            case RefInfo(_, _, Some(id), Some(offset)) =>
immler@34568
    82
              prover.get.command(id) match {
immler@34568
    83
                case Some(ref_cmd) =>
immler@34568
    84
                  new InternalHyperlink(start, end, line,
immler@34568
    85
                    theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
immler@34568
    86
                case _ => null
immler@34568
    87
              }
immler@34568
    88
            case _ => null
immler@34568
    89
          }
immler@34568
    90
        }
immler@34568
    91
      } else null
immler@34568
    92
    }
immler@34568
    93
  }
immler@34568
    94
}