src/Tools/jEdit/src/isabelle_hyperlinks.scala
author wenzelm
Thu Dec 01 14:29:14 2011 +0100 (2011-12-01 ago)
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46178 1c5c88f6feb5
permissions -rw-r--r--
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
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@45468
    60
            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
wenzelm@45468
    61
              Markup_Tree.Select[Hyperlink](
wenzelm@45468
    62
                {
wenzelm@45709
    63
                  // FIXME Protocol.Hyperlink extractor
wenzelm@45468
    64
                  case Text.Info(info_range,
wenzelm@45666
    65
                      XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
wenzelm@45468
    66
                    if (props.find(
wenzelm@45666
    67
                      { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
wenzelm@45666
    68
                        case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
wenzelm@45468
    69
                        case _ => false }).isEmpty) =>
wenzelm@45468
    70
                    val Text.Range(begin, end) = info_range
wenzelm@45468
    71
                    val line = buffer.getLineOfOffset(begin)
wenzelm@45468
    72
                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
wenzelm@45468
    73
                      case (Some(def_file), Some(def_line)) =>
wenzelm@45468
    74
                        new External_Hyperlink(begin, end, line, def_file, def_line)
wenzelm@45468
    75
                      case _ if !snapshot.is_outdated =>
wenzelm@45468
    76
                        (props, props) match {
wenzelm@45468
    77
                          case (Position.Id(def_id), Position.Offset(def_offset)) =>
wenzelm@45468
    78
                            snapshot.state.find_command(snapshot.version, def_id) match {
wenzelm@45468
    79
                              case Some((def_node, def_cmd)) =>
wenzelm@45468
    80
                                def_node.command_start(def_cmd) match {
wenzelm@45468
    81
                                  case Some(def_cmd_start) =>
wenzelm@45468
    82
                                    new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
wenzelm@45468
    83
                                      def_cmd_start + def_cmd.decode(def_offset))
wenzelm@45468
    84
                                  case None => null
wenzelm@45468
    85
                                }
wenzelm@38845
    86
                              case None => null
wenzelm@38845
    87
                            }
wenzelm@45468
    88
                          case _ => null
wenzelm@38845
    89
                        }
wenzelm@38845
    90
                      case _ => null
wenzelm@38845
    91
                    }
wenzelm@45474
    92
                },
wenzelm@45666
    93
                Some(Set(Isabelle_Markup.ENTITY))))
wenzelm@39177
    94
          markup match {
wenzelm@39177
    95
            case Text.Info(_, Some(link)) #:: _ => link
wenzelm@39177
    96
            case _ => null
wenzelm@39177
    97
          }
wenzelm@38843
    98
        case None => null
wenzelm@38843
    99
      }
immler@34568
   100
    }
immler@34568
   101
  }
immler@34568
   102
}