src/Tools/jEdit/src/isabelle_hyperlinks.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 47867 dd9cbe708e6b
permissions -rw-r--r--
more explicit java.io.{File => JFile};
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
wenzelm@48409
    12
import java.io.{File => JFile}
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@47867
    43
        Library.error_dialog(view, "File not found",
wenzelm@47867
    44
          Library.scrollable_text("Could not find source file " + def_file))
wenzelm@34602
    45
      case Some(file) =>
wenzelm@42327
    46
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
immler@34573
    47
    }
wenzelm@34602
    48
  }
immler@34569
    49
}
immler@34569
    50
wenzelm@34760
    51
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    52
{
wenzelm@38575
    53
  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
wenzelm@37175
    54
  {
wenzelm@38223
    55
    Swing_Thread.assert()
wenzelm@38843
    56
    Isabelle.buffer_lock(buffer) {
wenzelm@38843
    57
      Document_Model(buffer) match {
wenzelm@38843
    58
        case Some(model) =>
wenzelm@38843
    59
          val snapshot = model.snapshot()
wenzelm@38845
    60
          val markup =
wenzelm@46178
    61
            snapshot.select_markup[Hyperlink](
wenzelm@46178
    62
              Text.Range(buffer_offset, buffer_offset + 1),
wenzelm@46178
    63
              Some(Set(Isabelle_Markup.ENTITY)),
wenzelm@46178
    64
              {
wenzelm@46211
    65
                // FIXME Isabelle_Rendering.hyperlink
wenzelm@46178
    66
                case Text.Info(info_range,
wenzelm@46178
    67
                    XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
wenzelm@46178
    68
                  if (props.find(
wenzelm@46178
    69
                    { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
wenzelm@46178
    70
                      case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
wenzelm@46178
    71
                      case _ => false }).isEmpty) =>
wenzelm@46178
    72
                  val Text.Range(begin, end) = info_range
wenzelm@46178
    73
                  val line = buffer.getLineOfOffset(begin)
wenzelm@46178
    74
                  (Position.File.unapply(props), Position.Line.unapply(props)) match {
wenzelm@47541
    75
                    case (Some(def_file), def_line) =>
wenzelm@47541
    76
                      new External_Hyperlink(begin, end, line, def_file, def_line.getOrElse(1))
wenzelm@46178
    77
                    case _ if !snapshot.is_outdated =>
wenzelm@46178
    78
                      (props, props) match {
wenzelm@46178
    79
                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
wenzelm@46178
    80
                          snapshot.state.find_command(snapshot.version, def_id) match {
wenzelm@46178
    81
                            case Some((def_node, def_cmd)) =>
wenzelm@46178
    82
                              def_node.command_start(def_cmd) match {
wenzelm@46178
    83
                                case Some(def_cmd_start) =>
wenzelm@46178
    84
                                  new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
wenzelm@46178
    85
                                    def_cmd_start + def_cmd.decode(def_offset))
wenzelm@46178
    86
                                case None => null
wenzelm@46178
    87
                              }
wenzelm@46178
    88
                            case None => null
wenzelm@46178
    89
                          }
wenzelm@46178
    90
                        case _ => null
wenzelm@46178
    91
                      }
wenzelm@46178
    92
                    case _ => null
wenzelm@46178
    93
                  }
wenzelm@46178
    94
              })
wenzelm@39177
    95
          markup match {
wenzelm@46198
    96
            case Text.Info(_, link) #:: _ => link
wenzelm@39177
    97
            case _ => null
wenzelm@39177
    98
          }
wenzelm@38843
    99
        case None => null
wenzelm@38843
   100
      }
immler@34568
   101
    }
immler@34568
   102
  }
immler@34568
   103
}