src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
changeset 34759 bfea7839d9e1
parent 34714 983becb5ae9a
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,80 @@
     1.4 +/*
     1.5 + * Hyperlink setup for Isabelle proof documents
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + */
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +import java.io.File
    1.13 +
    1.14 +import gatchan.jedit.hyperlinks.Hyperlink
    1.15 +import gatchan.jedit.hyperlinks.HyperlinkSource
    1.16 +import gatchan.jedit.hyperlinks.AbstractHyperlink
    1.17 +
    1.18 +import org.gjt.sp.jedit.View
    1.19 +import org.gjt.sp.jedit.jEdit
    1.20 +import org.gjt.sp.jedit.Buffer
    1.21 +import org.gjt.sp.jedit.TextUtilities
    1.22 +
    1.23 +import isabelle.prover.Command
    1.24 +
    1.25 +
    1.26 +class InternalHyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    1.27 +  extends AbstractHyperlink(start, end, line, "")
    1.28 +{
    1.29 +  override def click(view: View) {
    1.30 +    view.getTextArea.moveCaretPosition(ref_offset)
    1.31 +  }
    1.32 +}
    1.33 +
    1.34 +class ExternalHyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    1.35 +  extends AbstractHyperlink(start, end, line, "")
    1.36 +{
    1.37 +  override def click(view: View) = {
    1.38 +    Isabelle.system.source_file(ref_file) match {
    1.39 +      case None => System.err.println("Could not find source file " + ref_file)
    1.40 +      case Some(file) =>
    1.41 +        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    1.42 +    }
    1.43 +  }
    1.44 +}
    1.45 +
    1.46 +class IsabelleHyperlinkSource extends HyperlinkSource
    1.47 +{
    1.48 +	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink = {
    1.49 +    val prover = Isabelle.prover_setup(buffer).map(_.prover)
    1.50 +    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
    1.51 +    if (prover.isEmpty || theory_view_opt.isEmpty) null
    1.52 +    else if (prover.get == null || theory_view_opt.get == null) null
    1.53 +    else {
    1.54 +      val theory_view = theory_view_opt.get
    1.55 +      val document = theory_view.current_document()
    1.56 +      val offset = theory_view.from_current(document, original_offset)
    1.57 +      document.command_at(offset) match {
    1.58 +        case Some(command) =>
    1.59 +          command.ref_at(document, offset - command.start(document)) match {
    1.60 +            case Some(ref) =>
    1.61 +              val command_start = command.start(document)
    1.62 +              val begin = theory_view.to_current(document, command_start + ref.start)
    1.63 +              val line = buffer.getLineOfOffset(begin)
    1.64 +              val end = theory_view.to_current(document, command_start + ref.stop)
    1.65 +              ref.info match {
    1.66 +                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    1.67 +                  new ExternalHyperlink(begin, end, line, ref_file, ref_line)
    1.68 +                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    1.69 +                  prover.get.command(id) match {
    1.70 +                    case Some(ref_cmd) =>
    1.71 +                      new InternalHyperlink(begin, end, line,
    1.72 +                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    1.73 +                    case None => null
    1.74 +                  }
    1.75 +                case _ => null
    1.76 +              }
    1.77 +            case None => null
    1.78 +          }
    1.79 +        case None => null
    1.80 +      }
    1.81 +    }
    1.82 +  }
    1.83 +}