Isabelle/jEdit action "isabelle.goto-entity"
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.
Written by makarius on Dec 18 2020, 11:38 AM.