src/Tools/jEdit/src/rendering.scala
changeset 55877 65c9968286d5
parent 55876 142139457653
child 55878 6d092a5166f1
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:41:58 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 03 10:59:33 2014 +0100
     1.3 @@ -327,6 +327,15 @@
     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 +        PIDE.editor.hyperlink_source_file(name, line)
    1.11 +      case Position.Def_Id_Offset(id, offset) =>
    1.12 +        PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.13 +      case _ => None
    1.14 +    }
    1.15 +
    1.16    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
    1.17    {
    1.18      snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    1.19 @@ -347,27 +356,12 @@
    1.20              { case (Markup.KIND, Markup.ML_OPEN) => true
    1.21                case (Markup.KIND, Markup.ML_STRUCTURE) => true
    1.22                case _ => false }) =>
    1.23 -
    1.24 -            val opt_link =
    1.25 -              props match {
    1.26 -                case Position.Def_Line_File(line, name) =>
    1.27 -                  PIDE.editor.hyperlink_source_file(name, line)
    1.28 -                case Position.Def_Id_Offset(id, offset) =>
    1.29 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.30 -                case _ => None
    1.31 -              }
    1.32 -            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.33 +            hyperlink_file(props).map(link =>
    1.34 +              (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.35  
    1.36            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    1.37 -            val opt_link =
    1.38 -              props match {
    1.39 -                case Position.Line_File(line, name) =>
    1.40 -                  PIDE.editor.hyperlink_source_file(name, line)
    1.41 -                case Position.Id_Offset(id, offset) =>
    1.42 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    1.43 -                case _ => None
    1.44 -              }
    1.45 -            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
    1.46 +            hyperlink_file(props).map(link =>
    1.47 +              (links :+ Text.Info(snapshot.convert(info_range), link)))
    1.48  
    1.49            case _ => None
    1.50          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }