added action isabelle.goto-entity to follow links in a narrow formal sense;
authorwenzelm
Wed, 16 Dec 2020 13:47:33 +0100
changeset 73170 0cc298e29aff
parent 73169 776198313227
child 73171 fa3fbbfc1f17
added action isabelle.goto-entity to follow links in a narrow formal sense;
NEWS
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/jedit_rendering.scala
--- 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.
 
--- 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);
--- 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)
   {
--- 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
--- 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 */