src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
author wenzelm
Sun Aug 15 22:48:56 2010 +0200 (2010-08-15)
changeset 38426 2858ec7b6dd8
parent 38370 8b15d0f98962
child 38427 7066fbd315ae
permissions -rw-r--r--
specific types Text.Offset and Text.Range;
minor tuning;
     1 /*  Title:      Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
     2     Author:     Fabian Immler, TU Munich
     3 
     4 Hyperlink setup for Isabelle proof documents.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.File
    13 
    14 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
    15 
    16 import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
    17 
    18 
    19 private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
    20   extends AbstractHyperlink(start, end, line, "")
    21 {
    22   override def click(view: View) {
    23     view.getTextArea.moveCaretPosition(ref_offset)
    24   }
    25 }
    26 
    27 class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
    28   extends AbstractHyperlink(start, end, line, "")
    29 {
    30   override def click(view: View) = {
    31     Isabelle.system.source_file(ref_file) match {
    32       case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
    33       case Some(file) =>
    34         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
    35     }
    36   }
    37 }
    38 
    39 class Isabelle_Hyperlinks extends HyperlinkSource
    40 {
    41   def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
    42   {
    43     Swing_Thread.assert()
    44     Document_Model(buffer) match {
    45       case Some(model) =>
    46         val snapshot = model.snapshot()
    47         val offset = snapshot.revert(original_offset)
    48         snapshot.node.command_at(offset) match {
    49           case Some((command, command_start)) =>
    50             snapshot.state(command).ref_at(offset - command_start) match {
    51               case Some(ref) =>
    52                 val begin = snapshot.convert(command_start + ref.range.start)
    53                 val line = buffer.getLineOfOffset(begin)
    54                 val end = snapshot.convert(command_start + ref.range.stop)
    55                 ref.info match {
    56                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    57                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
    58                   case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    59                     snapshot.lookup_command(id) match {  // FIXME Command_ID vs. Exec_ID (!??)
    60                       case Some(ref_cmd) =>
    61                         snapshot.node.command_start(ref_cmd) match {
    62                           case Some(ref_cmd_start) =>
    63                             new Internal_Hyperlink(begin, end, line,
    64                               snapshot.convert(ref_cmd_start + offset - 1))
    65                           case None => null // FIXME external ref
    66                         }
    67                       case _ => null
    68                     }
    69                   case _ => null
    70                 }
    71               case None => null
    72             }
    73           case None => null
    74         }
    75       case None => null
    76     }
    77   }
    78 }