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;
     1 /*  Title:      Tools/jEdit/src/isabelle_hyperlinks.scala
     2     Author:     Fabian Immler, TU Munich
     3 
     4 Hyperlink setup for Isabelle proof documents.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.File
    13 
    14 import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
    15 
    16 import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
    17 
    18 
    19 private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
    20   extends AbstractHyperlink(start, end, line, "")
    21 {
    22   override def click(view: View) {
    23     view.getTextArea.moveCaretPosition(def_offset)
    24   }
    25 }
    26 
    27 class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
    28   extends AbstractHyperlink(start, end, line, "")
    29 {
    30   override def click(view: View) = {
    31     Isabelle_System.source_file(Path.explode(def_file)) match {
    32       case None =>
    33         Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
    34       case Some(file) =>
    35         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
    36     }
    37   }
    38 }
    39 
    40 class Isabelle_Hyperlinks extends HyperlinkSource
    41 {
    42   def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
    43   {
    44     Swing_Thread.assert()
    45     Isabelle.buffer_lock(buffer) {
    46       Document_Model(buffer) match {
    47         case Some(model) =>
    48           val snapshot = model.snapshot()
    49           val markup =
    50             snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
    51               // FIXME Isar_Document.Hyperlink extractor
    52               case Text.Info(info_range,
    53                   XML.Elem(Markup(Markup.ENTITY, props), _))
    54                 if (props.find(
    55                   { case (Markup.KIND, Markup.ML_OPEN) => true
    56                     case (Markup.KIND, Markup.ML_STRUCT) => true
    57                     case _ => false }).isEmpty) =>
    58                 val Text.Range(begin, end) = info_range
    59                 val line = buffer.getLineOfOffset(begin)
    60                 (Position.File.unapply(props), Position.Line.unapply(props)) match {
    61                   case (Some(def_file), Some(def_line)) =>
    62                     new External_Hyperlink(begin, end, line, def_file, def_line)
    63                   case _ =>
    64                     (props, props) match {
    65                       case (Position.Id(def_id), Position.Offset(def_offset)) =>
    66                         snapshot.lookup_command(def_id) match {
    67                           case Some(def_cmd) =>
    68                             snapshot.node.command_start(def_cmd) match {
    69                               case Some(def_cmd_start) =>
    70                                 new Internal_Hyperlink(begin, end, line,
    71                                   snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
    72                               case None => null
    73                             }
    74                           case None => null
    75                         }
    76                       case _ => null
    77                     }
    78                 }
    79             }
    80           markup match {
    81             case Text.Info(_, Some(link)) #:: _ => link
    82             case _ => null
    83           }
    84         case None => null
    85       }
    86     }
    87   }
    88 }