src/Tools/jEdit/src/jedit_editor.scala
changeset 61011 018b0c996b54
parent 60988 1d7a7e33fd67
child 61544 19d84de5f534
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 23 22:47:01 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 24 00:20:20 2015 +0200
     1.3 @@ -279,6 +279,23 @@
     1.4      }
     1.5    }
     1.6  
     1.7 +  def is_hyperlink_position(snapshot: Document.Snapshot,
     1.8 +    text_offset: Text.Offset, pos: Position.T): Boolean =
     1.9 +  {
    1.10 +    pos match {
    1.11 +      case Position.Id_Offset0(id, offset) if offset > 0 =>
    1.12 +        snapshot.state.find_command(snapshot.version, id) match {
    1.13 +          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
    1.14 +            node.command_start(command) match {
    1.15 +              case Some(start) => text_offset == start + command.chunk.decode(offset)
    1.16 +              case None => false
    1.17 +            }
    1.18 +          case _ => false
    1.19 +        }
    1.20 +      case _ => false
    1.21 +    }
    1.22 +  }
    1.23 +
    1.24    def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
    1.25        : Option[Hyperlink] =
    1.26      pos match {