Email Gateway (Jan 23 2026 at 21:30): Email Gateway (Jan 23 2026 at 21:30):From: Makarius <makarius@sketis.net>
* General *
* Isabelle/jEdit Prover IDE *
The jEdit action "goto-entity" has been superseded by "follow-link",
while retaining the keyboard shortcut CS+d. The new action is more
general: it uses the same notion of link as C-hover-click via mouse.
Minor INCOMPATIBILITY.
Tooltip messages render formal entities with additional PIDE markup,
to distinguish multiple def-positions due to locale interpretations etc.
This refers to Isabelle/ad96a992ab53.
Makarius
Email Gateway (Jan 23 2026 at 21:54):From: Makarius <makarius@sketis.net>
On 23/01/2026 22:20, Makarius wrote:
- The jEdit action "goto-entity" has been superseded by "follow-link",
while retaining the keyboard shortcut CS+d. The new action is more
general: it uses the same notion of link as C-hover-click via mouse.
Minor INCOMPATIBILITY.
This one is not directly relevant here, but it belongs to the overall
improvements on hyperlinks from this week (and some more next week).
Makarius
Email Gateway (Jan 24 2026 at 11:40):From: Makarius <makarius@sketis.net>
On 23 Jan 2026, at 21:20, Makarius <makarius@sketis.net> wrote:
- The jEdit action "goto-entity" has been superseded by "follow-link",
while retaining the keyboard shortcut CS+d. The new action is more
general: it uses the same notion of link as C-hover-click via mouse.
On 24/01/2026 12:31, Lawrence Paulson wrote:
Sounds good. But what is this CS+d? I just tried it; it seems the same as
the mouse click.
It is now exactly the same as C-hover mouse click. The idea is to have a more
convenient shortcut for it, one that is also "accessible" for someone who
cannot use the mouse.
Makarius
Last updated: Feb 04 2026 at 02:22 UTC