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;
     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(name: String, start: Int, end: Int, line: Int, offset: Int)
    20   extends AbstractHyperlink(start, end, line, "")
    21 {
    22   override def click(view: View)
    23   {
    24     val text_area = view.getTextArea
    25     if (Isabelle.buffer_name(view.getBuffer) == name)
    26       text_area.moveCaretPosition(offset)
    27     else
    28       Isabelle.jedit_buffer(name) match {
    29         case Some(buffer) =>
    30           view.setBuffer(buffer)
    31           text_area.moveCaretPosition(offset)
    32         case None =>
    33       }
    34   }
    35 }
    36 
    37 class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
    38   extends AbstractHyperlink(start, end, line, "")
    39 {
    40   override def click(view: View) = {
    41     Isabelle_System.source_file(Path.explode(def_file)) match {
    42       case None =>
    43         Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
    44       case Some(file) =>
    45         jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
    46     }
    47   }
    48 }
    49 
    50 class Isabelle_Hyperlinks extends HyperlinkSource
    51 {
    52   def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
    53   {
    54     Swing_Thread.assert()
    55     Isabelle.buffer_lock(buffer) {
    56       Document_Model(buffer) match {
    57         case Some(model) =>
    58           val snapshot = model.snapshot()
    59           val markup =
    60             snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
    61               Markup_Tree.Select[Hyperlink](
    62                 {
    63                   // FIXME Protocol.Hyperlink extractor
    64                   case Text.Info(info_range,
    65                       XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    66                     if (props.find(
    67                       { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    68                         case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
    69                         case _ => false }).isEmpty) =>
    70                     val Text.Range(begin, end) = info_range
    71                     val line = buffer.getLineOfOffset(begin)
    72                     (Position.File.unapply(props), Position.Line.unapply(props)) match {
    73                       case (Some(def_file), Some(def_line)) =>
    74                         new External_Hyperlink(begin, end, line, def_file, def_line)
    75                       case _ if !snapshot.is_outdated =>
    76                         (props, props) match {
    77                           case (Position.Id(def_id), Position.Offset(def_offset)) =>
    78                             snapshot.state.find_command(snapshot.version, def_id) match {
    79                               case Some((def_node, def_cmd)) =>
    80                                 def_node.command_start(def_cmd) match {
    81                                   case Some(def_cmd_start) =>
    82                                     new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    83                                       def_cmd_start + def_cmd.decode(def_offset))
    84                                   case None => null
    85                                 }
    86                               case None => null
    87                             }
    88                           case _ => null
    89                         }
    90                       case _ => null
    91                     }
    92                 },
    93                 Some(Set(Isabelle_Markup.ENTITY))))
    94           markup match {
    95             case Text.Info(_, Some(link)) #:: _ => link
    96             case _ => null
    97           }
    98         case None => null
    99       }
   100     }
   101   }
   102 }