NEWS: Isabelle/jEdit hyperlinks and navigation

Makarius makarius at sketis.net
Sat Feb 28 22:07:17 CET 2026


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



More information about the isabelle-dev mailing list