recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
authorwenzelm
Mon Mar 03 12:24:14 2014 +0100 (2014-03-03 ago)
changeset 558836f50d445f0e3
parent 55882 912c9aa8de32
child 55884 f2c0eaedd579
recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 12:18:59 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 12:24:14 2014 +0100
     1.3 @@ -327,16 +327,6 @@
     1.4  
     1.5    /* hyperlinks */
     1.6  
     1.7 -  private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
     1.8 -    props match {
     1.9 -      case Position.Def_Line_File(line, name) =>
    1.10 -        val offset = Position.Def_Offset.unapply(props) getOrElse 0
    1.11 -        PIDE.editor.hyperlink_source_file(name, line, offset)
    1.12 -      case Position.Def_Id_Offset(id, offset) =>
    1.13 -        PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.14 -      case _ => None
    1.15 -    }
    1.16 -
    1.17    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.18    {
    1.19      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    1.20 @@ -357,12 +347,28 @@
    1.21              { case (Markup.KIND, Markup.ML_OPEN) => true
    1.22                case (Markup.KIND, Markup.ML_STRUCTURE) => true
    1.23                case _ => false }) =>
    1.24 -            hyperlink_file(props).map(link =>
    1.25 -              (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.26 +            val opt_link =
    1.27 +              props match {
    1.28 +                case Position.Def_Line_File(line, name) =>
    1.29 +                  val offset = Position.Def_Offset.unapply(props) getOrElse 0
    1.30 +                  PIDE.editor.hyperlink_source_file(name, line, offset)
    1.31 +                case Position.Def_Id_Offset(id, offset) =>
    1.32 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.33 +                case _ => None
    1.34 +              }
    1.35 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.36  
    1.37            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    1.38 -            hyperlink_file(props).map(link =>
    1.39 -              (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.40 +            val opt_link =
    1.41 +              props match {
    1.42 +                case Position.Line_File(line, name) =>
    1.43 +                  val offset = Position.Offset.unapply(props) getOrElse 0
    1.44 +                  PIDE.editor.hyperlink_source_file(name, line, offset)
    1.45 +                case Position.Id_Offset(id, offset) =>
    1.46 +                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.47 +                case _ => None
    1.48 +              }
    1.49 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.50  
    1.51            case _ => None
    1.52          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }