NEWS: Multiple hyperlinks in PIDE

Makarius makarius at sketis.net
Sat Jan 24 12:40:25 CET 2026


>> On 23 Jan 2026, at 21:20, Makarius <makarius at 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



More information about the isabelle-dev mailing list