--- 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 */