# HG changeset patch
# User wenzelm
# Date 1392666843 -3600
# Node ID 4a9f76263ece341abc636f364881d323fa562472
# Parent  cf1baba89a27f4def3a814b0dbc95a80e1b0931b
hyperlink for visible positions;

diff -r cf1baba89a27 -r 4a9f76263ece src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 20:19:02 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 17 20:54:03 2014 +0100
@@ -258,7 +258,21 @@
   }
 
 
-  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.URL)
+  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+
+  private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
+    if (Path.is_ok(name))
+      Isabelle_System.source_file(Path.explode(name)).map(path =>
+        PIDE.editor.hyperlink_file(Isabelle_System.platform_path(path), line))
+    else None
+
+  private def hyperlink_command(id: Document_ID.Generic, offset: Text.Offset)
+      : Option[PIDE.editor.Hyperlink] =
+    snapshot.state.find_command(snapshot.version, id) match {
+      case Some((node, command)) =>
+        PIDE.editor.hyperlink_command(snapshot, command, offset)
+      case None => None
+    }
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
@@ -281,26 +295,22 @@
               case (Markup.KIND, Markup.ML_STRUCT) => true
               case _ => false }) =>
 
-            props match {
-              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
-                Isabelle_System.source_file(Path.explode(name)) match {
-                  case Some(path) =>
-                    val jedit_file = Isabelle_System.platform_path(path)
-                    val link = PIDE.editor.hyperlink_file(jedit_file, line)
-                    Some(Text.Info(snapshot.convert(info_range), link) :: links)
-                  case None => None
-                }
+            val opt_link =
+              props match {
+                case Position.Def_Line_File(line, name) => hyperlink_file(line, name)
+                case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case _ => None
+              }
+            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
 
-              case Position.Def_Id_Offset(id, offset) =>
-                snapshot.state.find_command(snapshot.version, id) match {
-                  case Some((node, command)) =>
-                    PIDE.editor.hyperlink_command(snapshot, command, offset)
-                      .map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
-                  case None => None
-                }
-
-              case _ => None
-            }
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
+            val opt_link =
+              props match {
+                case Position.Line_File(line, name) => hyperlink_file(line, name)
+                case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
+                case _ => None
+              }
+            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
 
           case _ => None
         }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }