src/Tools/jEdit/src/isabelle_hyperlinks.scala
author wenzelm
Thu Sep 01 13:34:45 2011 +0200 (2011-09-01)
changeset 44615 a4ff8a787202
parent 44607 274eff0ea12e
child 45468 33e946d3f449
permissions -rw-r--r--
more abstract Document.Node.Name;
tuned signature;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/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@44580
    19
private class Internal_Hyperlink(name: String, start: Int, end: Int, line: Int, offset: Int)
immler@34569
    20
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    21
{
wenzelm@44580
    22
  override def click(view: View)
wenzelm@44580
    23
  {
wenzelm@44580
    24
    val text_area = view.getTextArea
wenzelm@44580
    25
    if (Isabelle.buffer_name(view.getBuffer) == name)
wenzelm@44580
    26
      text_area.moveCaretPosition(offset)
wenzelm@44580
    27
    else
wenzelm@44580
    28
      Isabelle.jedit_buffer(name) match {
wenzelm@44580
    29
        case Some(buffer) =>
wenzelm@44580
    30
          view.setBuffer(buffer)
wenzelm@44580
    31
          text_area.moveCaretPosition(offset)
wenzelm@44580
    32
        case None =>
wenzelm@44580
    33
      }
immler@34568
    34
  }
immler@34568
    35
}
immler@34568
    36
wenzelm@42327
    37
class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
immler@34569
    38
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    39
{
wenzelm@34602
    40
  override def click(view: View) = {
wenzelm@43661
    41
    Isabelle_System.source_file(Path.explode(def_file)) match {
wenzelm@38853
    42
      case None =>
wenzelm@42327
    43
        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
wenzelm@34602
    44
      case Some(file) =>
wenzelm@42327
    45
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
immler@34573
    46
    }
wenzelm@34602
    47
  }
immler@34569
    48
}
immler@34569
    49
wenzelm@34760
    50
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    51
{
wenzelm@38575
    52
  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
wenzelm@37175
    53
  {
wenzelm@38223
    54
    Swing_Thread.assert()
wenzelm@38843
    55
    Isabelle.buffer_lock(buffer) {
wenzelm@38843
    56
      Document_Model(buffer) match {
wenzelm@38843
    57
        case Some(model) =>
wenzelm@38843
    58
          val snapshot = model.snapshot()
wenzelm@38845
    59
          val markup =
wenzelm@38845
    60
            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
wenzelm@38843
    61
              // FIXME Isar_Document.Hyperlink extractor
wenzelm@42327
    62
              case Text.Info(info_range,
wenzelm@42327
    63
                  XML.Elem(Markup(Markup.ENTITY, props), _))
wenzelm@42327
    64
                if (props.find(
wenzelm@42327
    65
                  { case (Markup.KIND, Markup.ML_OPEN) => true
wenzelm@42327
    66
                    case (Markup.KIND, Markup.ML_STRUCT) => true
wenzelm@42327
    67
                    case _ => false }).isEmpty) =>
wenzelm@38845
    68
                val Text.Range(begin, end) = info_range
wenzelm@38845
    69
                val line = buffer.getLineOfOffset(begin)
wenzelm@38845
    70
                (Position.File.unapply(props), Position.Line.unapply(props)) match {
wenzelm@42327
    71
                  case (Some(def_file), Some(def_line)) =>
wenzelm@42327
    72
                    new External_Hyperlink(begin, end, line, def_file, def_line)
wenzelm@44580
    73
                  case _ if !snapshot.is_outdated =>
wenzelm@38845
    74
                    (props, props) match {
wenzelm@42327
    75
                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
wenzelm@44582
    76
                        snapshot.state.find_command(snapshot.version, def_id) match {
wenzelm@44607
    77
                          case Some((def_node, def_cmd)) =>
wenzelm@44580
    78
                            def_node.command_start(def_cmd) match {
wenzelm@42327
    79
                              case Some(def_cmd_start) =>
wenzelm@44615
    80
                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
wenzelm@44580
    81
                                  def_cmd_start + def_cmd.decode(def_offset))
wenzelm@38845
    82
                              case None => null
wenzelm@38845
    83
                            }
wenzelm@38845
    84
                          case None => null
wenzelm@38845
    85
                        }
wenzelm@38845
    86
                      case _ => null
wenzelm@38845
    87
                    }
wenzelm@44580
    88
                  case _ => null
wenzelm@38845
    89
                }
wenzelm@39177
    90
            }
wenzelm@39177
    91
          markup match {
wenzelm@39177
    92
            case Text.Info(_, Some(link)) #:: _ => link
wenzelm@39177
    93
            case _ => null
wenzelm@39177
    94
          }
wenzelm@38843
    95
        case None => null
wenzelm@38843
    96
      }
immler@34568
    97
    }
immler@34568
    98
  }
immler@34568
    99
}