HomeIsabelle/Phabricator
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.
User
Projects
None
Subscribers
None

Event Timeline