src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
author wenzelm
Wed Dec 16 21:11:04 2009 +0100 (2009-12-16)
changeset 34791 b97d5b38dea4
parent 34788 3779c54a2d21
child 34816 d33312514220
permissions -rw-r--r--
explicit object Session.Global_Settings;
misc tuning;
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@34791
     9
import isabelle.proofdocument.Command
wenzelm@34760
    10
immler@34569
    11
import java.io.File
immler@34569
    12
wenzelm@34791
    13
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
immler@34568
    14
wenzelm@34791
    15
import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
immler@34568
    16
wenzelm@34588
    17
wenzelm@34760
    18
private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
immler@34569
    19
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    20
{
wenzelm@34582
    21
  override def click(view: View) {
immler@34568
    22
    view.getTextArea.moveCaretPosition(ref_offset)
immler@34568
    23
  }
immler@34568
    24
}
immler@34568
    25
wenzelm@34760
    26
class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
immler@34569
    27
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    28
{
wenzelm@34602
    29
  override def click(view: View) = {
wenzelm@34602
    30
    Isabelle.system.source_file(ref_file) match {
wenzelm@34760
    31
      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
wenzelm@34602
    32
      case Some(file) =>
immler@34573
    33
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
immler@34573
    34
    }
wenzelm@34602
    35
  }
immler@34569
    36
}
immler@34569
    37
wenzelm@34760
    38
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    39
{
wenzelm@34760
    40
	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
wenzelm@34760
    41
	{
wenzelm@34788
    42
    Document_Model(buffer) match {
wenzelm@34784
    43
      case Some(model) =>
wenzelm@34784
    44
        val document = model.current_document()
wenzelm@34784
    45
        val offset = model.from_current(document, original_offset)
wenzelm@34777
    46
        document.command_at(offset) match {
wenzelm@34777
    47
          case Some(command) =>
wenzelm@34777
    48
            command.ref_at(document, offset - command.start(document)) match {
wenzelm@34777
    49
              case Some(ref) =>
wenzelm@34777
    50
                val command_start = command.start(document)
wenzelm@34784
    51
                val begin = model.to_current(document, command_start + ref.start)
wenzelm@34777
    52
                val line = buffer.getLineOfOffset(begin)
wenzelm@34784
    53
                val end = model.to_current(document, command_start + ref.stop)
wenzelm@34777
    54
                ref.info match {
wenzelm@34777
    55
                  case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
wenzelm@34777
    56
                    new External_Hyperlink(begin, end, line, ref_file, ref_line)
wenzelm@34777
    57
                  case Command.RefInfo(_, _, Some(id), Some(offset)) =>
wenzelm@34777
    58
                    Isabelle.session.command(id) match {
wenzelm@34777
    59
                      case Some(ref_cmd) =>
wenzelm@34777
    60
                        new Internal_Hyperlink(begin, end, line,
wenzelm@34784
    61
                          model.to_current(document, ref_cmd.start(document) + offset - 1))
wenzelm@34777
    62
                      case None => null
wenzelm@34777
    63
                    }
wenzelm@34777
    64
                  case _ => null
wenzelm@34777
    65
                }
wenzelm@34777
    66
              case None => null
wenzelm@34777
    67
            }
wenzelm@34777
    68
          case None => null
wenzelm@34777
    69
        }
wenzelm@34777
    70
      case None => null
immler@34568
    71
    }
immler@34568
    72
  }
immler@34568
    73
}