--- a/src/Tools/jEdit/src/rendering.scala Mon Mar 03 10:41:58 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Mar 03 10:59:33 2014 +0100
@@ -327,6 +327,15 @@
/* hyperlinks */
+ private def hyperlink_file(props: Properties.T): Option[PIDE.editor.Hyperlink] =
+ props match {
+ case Position.Def_Line_File(line, name) =>
+ PIDE.editor.hyperlink_source_file(name, line)
+ case Position.Def_Id_Offset(id, offset) =>
+ PIDE.editor.hyperlink_command_id(snapshot, id, offset)
+ case _ => None
+ }
+
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
@@ -347,27 +356,12 @@
{ 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) =>
- PIDE.editor.hyperlink_source_file(name, line)
- case Position.Def_Id_Offset(id, offset) =>
- PIDE.editor.hyperlink_command_id(snapshot, id, offset)
- case _ => None
- }
- opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
+ hyperlink_file(props).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) =>
- PIDE.editor.hyperlink_source_file(name, line)
- case Position.Id_Offset(id, offset) =>
- PIDE.editor.hyperlink_command_id(snapshot, id, offset)
- case _ => None
- }
- opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
+ hyperlink_file(props).map(link =>
+ (links :+ Text.Info(snapshot.convert(info_range), link)))
case _ => None
}) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }