From: Makarius <makarius@sketis.net>
* Isabelle/jEdit Prover IDE *
The built-in navigator provides a separate history for each editor
view, instead of just one global history. INCOMPATIBILITY.
The jEdit action "isabelle.goto-entity" with keyboard shortcut CS+d
has been removed. INCOMPATIBILITY, use the more general "follow-link"
with keyboard shortcut AS+DOWN instead.
The jEdit action "isabelle.follow-link" (keyboard shortcut AS+DOWN)
follows the hyperlink under the current caret, using the same notion of
link as C-hover-click via mouse.
The jEdit action "isabelle.show-links" (keyboard shortcut AS+UP) opens
a popup with the list of hyperlinks under the current caret, using the
same notion of link as C-hover-click via mouse, but showing all
possibilities.
This refers to Isabelle/a9d9e47f24a5.
Note that AS+LEFT and AS+RIGHT were already present to navigate backwards and
forwards, instead of using the arrow icons below the menu bar. Thus AS+arrow
keys can be used uniformly to jump around quickly, based on formal entity
definitions, or explicit links (files, URLs, docs, etc.).
It may help to move $ISABELLE_HOME_USER/jedit/keymaps out of the way, let the
application create it afresh, and then sort out new and old keyboard
shortcuts: there have been many changes recently, usually to improve
accessibility. This also helps to click less and type more quickly.
Makarius
From: Makarius <makarius@sketis.net>
On 28/02/2026 22:07, Makarius wrote:
Thus AS+arrow
keys can be used uniformly to jump around quickly, based on formal entity
definitions, or explicit links (files, URLs, docs, etc.).
As usual in this formal jEdit notation, "A" means "ALT" on Linux or Windows,
and "CONTROL" on macOS.
Makarius
Last updated: Mar 17 2026 at 17:04 UTC