src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
immler@34568
     1
/*
wenzelm@34588
     2
 * Hyperlink setup for Isabelle proof documents
immler@34568
     3
 *
wenzelm@34588
     4
 * @author Fabian Immler, TU Munich
immler@34568
     5
 */
immler@34568
     6
immler@34568
     7
package isabelle.jedit
immler@34569
     8
wenzelm@34760
     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
wenzelm@34760
    21
import isabelle.proofdocument.Command
immler@34568
    22
wenzelm@34588
    23
wenzelm@34760
    24
private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
immler@34569
    25
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    26
{
wenzelm@34582
    27
  override def click(view: View) {
immler@34568
    28
    view.getTextArea.moveCaretPosition(ref_offset)
immler@34568
    29
  }
immler@34568
    30
}
immler@34568
    31
wenzelm@34760
    32
class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
immler@34569
    33
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    34
{
wenzelm@34602
    35
  override def click(view: View) = {
wenzelm@34602
    36
    Isabelle.system.source_file(ref_file) match {
wenzelm@34760
    37
      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
wenzelm@34602
    38
      case Some(file) =>
immler@34573
    39
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
immler@34573
    40
    }
wenzelm@34602
    41
  }
immler@34569
    42
}
immler@34569
    43
wenzelm@34760
    44
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    45
{
wenzelm@34760
    46
	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
wenzelm@34760
    47
	{
immler@34568
    48
    val prover = Isabelle.prover_setup(buffer).map(_.prover)
immler@34568
    49
    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
wenzelm@34714
    50
    if (prover.isEmpty || theory_view_opt.isEmpty) null
immler@34568
    51
    else if (prover.get == null || theory_view_opt.get == null) null
immler@34568
    52
    else {
immler@34568
    53
      val theory_view = theory_view_opt.get
immler@34650
    54
      val document = theory_view.current_document()
immler@34568
    55
      val offset = theory_view.from_current(document, original_offset)
wenzelm@34712
    56
      document.command_at(offset) match {
wenzelm@34712
    57
        case Some(command) =>
wenzelm@34712
    58
          command.ref_at(document, offset - command.start(document)) match {
wenzelm@34712
    59
            case Some(ref) =>
wenzelm@34712
    60
              val command_start = command.start(document)
wenzelm@34712
    61
              val begin = theory_view.to_current(document, command_start + ref.start)
wenzelm@34712
    62
              val line = buffer.getLineOfOffset(begin)
wenzelm@34712
    63
              val end = theory_view.to_current(document, command_start + ref.stop)
wenzelm@34712
    64
              ref.info match {
wenzelm@34712
    65
                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
wenzelm@34760
    66
                  new External_Hyperlink(begin, end, line, ref_file, ref_line)
wenzelm@34712
    67
                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
wenzelm@34712
    68
                  prover.get.command(id) match {
wenzelm@34712
    69
                    case Some(ref_cmd) =>
wenzelm@34760
    70
                      new Internal_Hyperlink(begin, end, line,
wenzelm@34712
    71
                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
wenzelm@34712
    72
                    case None => null
wenzelm@34712
    73
                  }
immler@34568
    74
                case _ => null
immler@34568
    75
              }
wenzelm@34712
    76
            case None => null
immler@34568
    77
          }
wenzelm@34712
    78
        case None => null
wenzelm@34712
    79
      }
immler@34568
    80
    }
immler@34568
    81
  }
immler@34568
    82
}