# HG changeset patch
# User wenzelm
# Date 1439208829 -7200
# Node ID 7865e03a7fc1d83e9ea3c4c690a98f579a812c53
# Parent  974d9acb2b87f4d008ef4cc293489eddbe40e477
tuned signature;

diff -r 974d9acb2b87 -r 7865e03a7fc1 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 10 13:54:12 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 10 14:13:49 2015 +0200
@@ -271,4 +271,24 @@
       case None => None
     }
   }
+
+  def hyperlink_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
+    pos match {
+      case Position.Line_File(line, name) =>
+        val offset = Position.Offset.unapply(pos) getOrElse 0
+        hyperlink_source_file(name, line, offset)
+      case Position.Id_Offset0(id, offset) =>
+        hyperlink_command_id(snapshot, id, offset)
+      case _ => None
+    }
+
+  def hyperlink_def_position(snapshot: Document.Snapshot, pos: Position.T): Option[Hyperlink] =
+    pos match {
+      case Position.Def_Line_File(line, name) =>
+        val offset = Position.Def_Offset.unapply(pos) getOrElse 0
+        hyperlink_source_file(name, line, offset)
+      case Position.Def_Id_Offset0(id, offset) =>
+        hyperlink_command_id(snapshot, id, offset)
+      case _ => None
+    }
 }
diff -r 974d9acb2b87 -r 7865e03a7fc1 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 13:54:12 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 14:13:49 2015 +0200
@@ -398,27 +398,11 @@
             { case (Markup.KIND, Markup.ML_OPEN) => true
               case (Markup.KIND, Markup.ML_STRUCTURE) => true
               case _ => false }) =>
-            val opt_link =
-              props match {
-                case Position.Def_Line_File(line, name) =>
-                  val offset = Position.Def_Offset.unapply(props) getOrElse 0
-                  PIDE.editor.hyperlink_source_file(name, line, offset)
-                case Position.Def_Id_Offset0(id, offset) =>
-                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
-                case _ => None
-              }
+            val opt_link = PIDE.editor.hyperlink_def_position(snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
-            val opt_link =
-              props match {
-                case Position.Line_File(line, name) =>
-                  val offset = Position.Offset.unapply(props) getOrElse 0
-                  PIDE.editor.hyperlink_source_file(name, line, offset)
-                case Position.Id_Offset0(id, offset) =>
-                  PIDE.editor.hyperlink_command_id(snapshot, id, offset)
-                case _ => None
-              }
+            val opt_link = PIDE.editor.hyperlink_position(snapshot, props)
             opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>