tuned signature;
authorwenzelm
Mon Aug 10 14:13:49 2015 +0200 (2015-08-10)
changeset 608747865e03a7fc1
parent 60873 974d9acb2b87
child 60875 ee23c1d21ac3
tuned signature;
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
     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  }
     2.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 13:54:12 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 14:13:49 2015 +0200
     2.3 @@ -398,27 +398,11 @@
     2.4              { case (Markup.KIND, Markup.ML_OPEN) => true
     2.5                case (Markup.KIND, Markup.ML_STRUCTURE) => true
     2.6                case _ => false }) =>
     2.7 -            val opt_link =
     2.8 -              props match {
     2.9 -                case Position.Def_Line_File(line, name) =>
    2.10 -                  val offset = Position.Def_Offset.unapply(props) getOrElse 0
    2.11 -                  PIDE.editor.hyperlink_source_file(name, line, offset)
    2.12 -                case Position.Def_Id_Offset0(id, offset) =>
    2.13 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    2.14 -                case _ => None
    2.15 -              }
    2.16 +            val opt_link = PIDE.editor.hyperlink_def_position(snapshot, props)
    2.17              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    2.18  
    2.19            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    2.20 -            val opt_link =
    2.21 -              props match {
    2.22 -                case Position.Line_File(line, name) =>
    2.23 -                  val offset = Position.Offset.unapply(props) getOrElse 0
    2.24 -                  PIDE.editor.hyperlink_source_file(name, line, offset)
    2.25 -                case Position.Id_Offset0(id, offset) =>
    2.26 -                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    2.27 -                case _ => None
    2.28 -              }
    2.29 +            val opt_link = PIDE.editor.hyperlink_position(snapshot, props)
    2.30              opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    2.31  
    2.32            case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>