src/Tools/jEdit/src/jedit_editor.scala
changeset 60874 7865e03a7fc1
parent 59319 677615cba30d
child 60893 3c8b9b4b577c
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 10 13:54:12 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 10 14:13:49 2015 +0200
     1.3 @@ -271,4 +271,24 @@
     1.4        case None => None
     1.5      }
     1.6    }
     1.7 +
     1.8 +  def hyperlink_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
     1.9 +    pos match {
    1.10 +      case Position.Line_File(line, name) =>
    1.11 +        val offset = Position.Offset.unapply(pos) getOrElse 0
    1.12 +        hyperlink_source_file(name, line, offset)
    1.13 +      case Position.Id_Offset0(id, offset) =>
    1.14 +        hyperlink_command_id(snapshot, id, offset)
    1.15 +      case _ => None
    1.16 +    }
    1.17 +
    1.18 +  def hyperlink_def_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
    1.19 +    pos match {
    1.20 +      case Position.Def_Line_File(line, name) =>
    1.21 +        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
    1.22 +        hyperlink_source_file(name, line, offset)
    1.23 +      case Position.Def_Id_Offset0(id, offset) =>
    1.24 +        hyperlink_command_id(snapshot, id, offset)
    1.25 +      case _ => None
    1.26 +    }
    1.27  }