src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
author wenzelm
Sun Aug 22 16:37:15 2010 +0200 (2010-08-22)
changeset 38575 80d962964216
parent 38427 7066fbd315ae
child 38577 4e4d3ea3725a
permissions -rw-r--r--
Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
wenzelm@36760
     4
Hyperlink setup for Isabelle proof documents.
wenzelm@36760
     5
*/
immler@34568
     6
immler@34568
     7
package isabelle.jedit
immler@34569
     8
wenzelm@34760
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
immler@34569
    12
import java.io.File
immler@34569
    13
wenzelm@34791
    14
import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
immler@34568
    15
wenzelm@34791
    16
import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
immler@34568
    17
wenzelm@34588
    18
wenzelm@34760
    19
private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
immler@34569
    20
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    21
{
wenzelm@34582
    22
  override def click(view: View) {
immler@34568
    23
    view.getTextArea.moveCaretPosition(ref_offset)
immler@34568
    24
  }
immler@34568
    25
}
immler@34568
    26
wenzelm@34760
    27
class External_Hyperlink(start: Int, end: Int, line: Int, ref_file: String, ref_line: Int)
immler@34569
    28
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    29
{
wenzelm@34602
    30
  override def click(view: View) = {
wenzelm@34602
    31
    Isabelle.system.source_file(ref_file) match {
wenzelm@34760
    32
      case None => System.err.println("Could not find source file " + ref_file)  // FIXME ??
wenzelm@34602
    33
      case Some(file) =>
immler@34573
    34
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + ref_line))
immler@34573
    35
    }
wenzelm@34602
    36
  }
immler@34569
    37
}
immler@34569
    38
wenzelm@34760
    39
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    40
{
wenzelm@38575
    41
  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
wenzelm@37175
    42
  {
wenzelm@38223
    43
    Swing_Thread.assert()
wenzelm@34788
    44
    Document_Model(buffer) match {
wenzelm@34784
    45
      case Some(model) =>
wenzelm@38151
    46
        val snapshot = model.snapshot()
wenzelm@38575
    47
        val offset = snapshot.revert(buffer_offset)
wenzelm@38152
    48
        snapshot.node.command_at(offset) match {
wenzelm@34855
    49
          case Some((command, command_start)) =>
wenzelm@38575
    50
            val root_node =
wenzelm@38575
    51
              Markup_Tree.Node[Hyperlink]((Text.Range(offset) - command_start), null)
wenzelm@38575
    52
wenzelm@38575
    53
            (snapshot.state(command).markup.select(root_node) {
wenzelm@38575
    54
              case XML.Elem(Markup(Markup.ML_REF, _),
wenzelm@38575
    55
                  List(XML.Elem(Markup(Markup.ML_DEF, props), _))) =>
wenzelm@38575
    56
//{{{
wenzelm@38575
    57
                val node_range = root_node.range // FIXME proper range
wenzelm@38575
    58
                val Text.Range(begin, end) = snapshot.convert(node_range + command_start)
wenzelm@34777
    59
                val line = buffer.getLineOfOffset(begin)
wenzelm@38575
    60
wenzelm@38575
    61
                (Position.get_file(props), Position.get_line(props)) match {
wenzelm@38575
    62
                  case (Some(ref_file), Some(ref_line)) =>
wenzelm@34777
    63
                    new External_Hyperlink(begin, end, line, ref_file, ref_line)
wenzelm@38575
    64
                  case _ =>
wenzelm@38575
    65
                    (Position.get_id(props), Position.get_offset(props)) match {
wenzelm@38575
    66
                      case (Some(ref_id), Some(ref_offset)) =>
wenzelm@38575
    67
                        snapshot.lookup_command(ref_id) match {
wenzelm@38575
    68
                          case Some(ref_cmd) =>
wenzelm@38575
    69
                            snapshot.node.command_start(ref_cmd) match {
wenzelm@38575
    70
                              case Some(ref_cmd_start) =>
wenzelm@38575
    71
                                new Internal_Hyperlink(begin, end, line,
wenzelm@38575
    72
                                  snapshot.convert(ref_cmd_start + ref_offset - 1)) // FIXME Command.decode_range
wenzelm@38575
    73
                              case None => null
wenzelm@38575
    74
                            }
wenzelm@38575
    75
                          case None => null
wenzelm@34858
    76
                        }
wenzelm@34816
    77
                      case _ => null
wenzelm@34777
    78
                    }
wenzelm@34777
    79
                }
wenzelm@38575
    80
//}}}
wenzelm@38575
    81
            }).head.info
wenzelm@34777
    82
          case None => null
wenzelm@34777
    83
        }
wenzelm@34777
    84
      case None => null
immler@34568
    85
    }
immler@34568
    86
  }
immler@34568
    87
}