[isabelle-dev] NEWS: Isabelle/jEdit action "isabelle.goto-entity"

[Lawrence Paulson]

I wish that some inspired student would put together a demo video or perhaps implement a “tip of the day” feature, because there are many many things (this will be yet another one) that are super useful almost impossible to discover. Your little trick for renaming bound variables is another; you demonstrated it to me but who could find it for himself?

Larry

> On 18 Dec 2020, at 10:40, Makarius <makarius at sketis.net> wrote:
> 
> *** Isabelle/jEdit Prover IDE ***
> 
> * Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
> of the formal entity at the caret position.
> 
> * The visual feedback on caret entity focus is normally restricted to
> definitions within the visible text area. The keyboard modifier "CS"
> overrides this: then all defining and referencing positions are shown.
> See also option "jedit_focus_modifier".
> 
> This refers to Isabelle/f7954a960890.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev