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;
     1 /*
     2  * Hyperlink setup for Isabelle proof documents
     3  *
     4  * @author Fabian Immler, TU Munich
     5  */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import java.io.File
    11 
    12 import gatchan.jedit.hyperlinks.Hyperlink
    13 import gatchan.jedit.hyperlinks.HyperlinkSource
    14 import gatchan.jedit.hyperlinks.AbstractHyperlink
    15 
    16 import org.gjt.sp.jedit.View
    17 import org.gjt.sp.jedit.jEdit
    18 import org.gjt.sp.jedit.Buffer
    19 import org.gjt.sp.jedit.TextUtilities
    20 
    21 import isabelle.proofdocument.Command
    22 
    23 
    24 private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    25   extends AbstractHyperlink(start, end, line, "")
    26 {
    27   override def click(view: View) {
    28     view.getTextArea.moveCaretPosition(ref_offset)
    29   }
    30 }
    31 
    32 class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    33   extends AbstractHyperlink(start, end, line, "")
    34 {
    35   override def click(view: View) = {
    36     Isabelle.system.source_file(ref_file) match {
    37       case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
    38       case Some(file) =>
    39         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    40     }
    41   }
    42 }
    43 
    44 class Isabelle_Hyperlinks extends HyperlinkSource
    45 {
    46 	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
    47 	{
    48     val prover = Isabelle.prover_setup(buffer).map(_.prover)
    49     val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
    50     if (prover.isEmpty || theory_view_opt.isEmpty) null
    51     else if (prover.get == null || theory_view_opt.get == null) null
    52     else {
    53       val theory_view = theory_view_opt.get
    54       val document = theory_view.current_document()
    55       val offset = theory_view.from_current(document, original_offset)
    56       document.command_at(offset) match {
    57         case Some(command) =>
    58           command.ref_at(document, offset - command.start(document)) match {
    59             case Some(ref) =>
    60               val command_start = command.start(document)
    61               val begin = theory_view.to_current(document, command_start + ref.start)
    62               val line = buffer.getLineOfOffset(begin)
    63               val end = theory_view.to_current(document, command_start + ref.stop)
    64               ref.info match {
    65                 case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    66                   new External_Hyperlink(begin, end, line, ref_file, ref_line)
    67                 case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    68                   prover.get.command(id) match {
    69                     case Some(ref_cmd) =>
    70                       new Internal_Hyperlink(begin, end, line,
    71                         theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    72                     case None => null
    73                   }
    74                 case _ => null
    75               }
    76             case None => null
    77           }
    78         case None => null
    79       }
    80     }
    81   }
    82 }