src/Tools/jEdit/src/isabelle_hyperlinks.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 43661 39fdbd814c7f
child 44580 3bc9a215a56d
permissions -rw-r--r--
propagate editor perspective through document model;
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@42327
    19
private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
immler@34569
    20
  extends AbstractHyperlink(start, end, line, "")
immler@34568
    21
{
wenzelm@34582
    22
  override def click(view: View) {
wenzelm@42327
    23
    view.getTextArea.moveCaretPosition(def_offset)
immler@34568
    24
  }
immler@34568
    25
}
immler@34568
    26
wenzelm@42327
    27
class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
immler@34569
    28
  extends AbstractHyperlink(start, end, line, "")
immler@34569
    29
{
wenzelm@34602
    30
  override def click(view: View) = {
wenzelm@43661
    31
    Isabelle_System.source_file(Path.explode(def_file)) match {
wenzelm@38853
    32
      case None =>
wenzelm@42327
    33
        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
wenzelm@34602
    34
      case Some(file) =>
wenzelm@42327
    35
        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
immler@34573
    36
    }
wenzelm@34602
    37
  }
immler@34569
    38
}
immler@34569
    39
wenzelm@34760
    40
class Isabelle_Hyperlinks extends HyperlinkSource
immler@34568
    41
{
wenzelm@38575
    42
  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
wenzelm@37175
    43
  {
wenzelm@38223
    44
    Swing_Thread.assert()
wenzelm@38843
    45
    Isabelle.buffer_lock(buffer) {
wenzelm@38843
    46
      Document_Model(buffer) match {
wenzelm@38843
    47
        case Some(model) =>
wenzelm@38843
    48
          val snapshot = model.snapshot()
wenzelm@38845
    49
          val markup =
wenzelm@38845
    50
            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
wenzelm@38843
    51
              // FIXME Isar_Document.Hyperlink extractor
wenzelm@42327
    52
              case Text.Info(info_range,
wenzelm@42327
    53
                  XML.Elem(Markup(Markup.ENTITY, props), _))
wenzelm@42327
    54
                if (props.find(
wenzelm@42327
    55
                  { case (Markup.KIND, Markup.ML_OPEN) => true
wenzelm@42327
    56
                    case (Markup.KIND, Markup.ML_STRUCT) => true
wenzelm@42327
    57
                    case _ => false }).isEmpty) =>
wenzelm@38845
    58
                val Text.Range(begin, end) = info_range
wenzelm@38845
    59
                val line = buffer.getLineOfOffset(begin)
wenzelm@38845
    60
                (Position.File.unapply(props), Position.Line.unapply(props)) match {
wenzelm@42327
    61
                  case (Some(def_file), Some(def_line)) =>
wenzelm@42327
    62
                    new External_Hyperlink(begin, end, line, def_file, def_line)
wenzelm@38845
    63
                  case _ =>
wenzelm@38845
    64
                    (props, props) match {
wenzelm@42327
    65
                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
wenzelm@42327
    66
                        snapshot.lookup_command(def_id) match {
wenzelm@42327
    67
                          case Some(def_cmd) =>
wenzelm@42327
    68
                            snapshot.node.command_start(def_cmd) match {
wenzelm@42327
    69
                              case Some(def_cmd_start) =>
wenzelm@38845
    70
                                new Internal_Hyperlink(begin, end, line,
wenzelm@42327
    71
                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
wenzelm@38845
    72
                              case None => null
wenzelm@38845
    73
                            }
wenzelm@38845
    74
                          case None => null
wenzelm@38845
    75
                        }
wenzelm@38845
    76
                      case _ => null
wenzelm@38845
    77
                    }
wenzelm@38845
    78
                }
wenzelm@39177
    79
            }
wenzelm@39177
    80
          markup match {
wenzelm@39177
    81
            case Text.Info(_, Some(link)) #:: _ => link
wenzelm@39177
    82
            case _ => null
wenzelm@39177
    83
          }
wenzelm@38843
    84
        case None => null
wenzelm@38843
    85
      }
immler@34568
    86
    }
immler@34568
    87
  }
immler@34568
    88
}