# HG changeset patch
# User wenzelm
# Date 1608122853 -3600
# Node ID 0cc298e29affcb6974542f314688798420dce4e6
# Parent  776198313227652b7bdfd170d518beb8191ebb6e
added action isabelle.goto-entity to follow links in a narrow formal sense;

diff -r 776198313227 -r 0cc298e29aff NEWS
--- a/NEWS	Wed Dec 16 13:22:38 2020 +0100
+++ b/NEWS	Wed Dec 16 13:47:33 2020 +0100
@@ -16,6 +16,9 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
+of the formal entity at the caret position.
+
 * Auto nitpick is enabled by default: it is now reasonably fast due to
 Kodkod invocation within Isabelle/Scala.
 
diff -r 776198313227 -r 0cc298e29aff src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Wed Dec 16 13:22:38 2020 +0100
+++ b/src/Tools/jEdit/src/actions.xml	Wed Dec 16 13:47:33 2020 +0100
@@ -67,6 +67,11 @@
 	    isabelle.jedit.Isabelle.newline(textArea);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.goto-entity">
+	  <CODE>
+	    isabelle.jedit.Isabelle.goto_entity(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.select-entity">
 	  <CODE>
 	    isabelle.jedit.Isabelle.select_entity(textArea);
diff -r 776198313227 -r 0cc298e29aff src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Dec 16 13:22:38 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Dec 16 13:47:33 2020 +0100
@@ -352,7 +352,18 @@
   }
 
 
-  /* selection */
+  /* formal entities */
+
+  def goto_entity(view: View)
+  {
+    val text_area = view.getTextArea
+    for {
+      doc_view <- Document_View.get(text_area)
+      rendering = doc_view.get_rendering()
+      caret_range = JEdit_Lib.caret_range(text_area)
+      link <- rendering.hyperlink_entity(caret_range)
+    } link.info.follow(view)
+  }
 
   def select_entity(text_area: JEditTextArea)
   {
diff -r 776198313227 -r 0cc298e29aff src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed Dec 16 13:22:38 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed Dec 16 13:47:33 2020 +0100
@@ -225,6 +225,8 @@
 isabelle.exclude-word.label=Exclude word
 isabelle.first-error.label=Go to first error
 isabelle.first-error.shortcut=CS+a
+isabelle.goto-entity.label=Go to definition of formal entity at caret
+isabelle.goto-entity.shortcut=CS+d
 isabelle.include-word-permanently.label=Include word permanently
 isabelle.include-word.label=Include word
 isabelle.increase-font-size.label=Increase font size
diff -r 776198313227 -r 0cc298e29aff src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 16 13:22:38 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Wed Dec 16 13:47:33 2020 +0100
@@ -285,6 +285,18 @@
         }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   }
 
+  def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
+  {
+    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+      range, Vector.empty, Rendering.entity_elements, _ =>
+        {
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
+            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
+            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
+          case _ => None
+        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
+  }
+
 
   /* active elements */