[isabelle-dev] NEWS: isabelle.select-entity

Makarius makarius at sketis.net
Mon Jun 6 20:46:25 CEST 2016

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
occurences of the formal entity at the caret position. This facilitates
systematic renaming.

This refers to Isabelle/48bc9045866e.

As usual, new keyboard shortcuts need to be provided manually if some
Isabelle/jEdit configuration is already present.

This really just "facilitates systematic renaming". Actual "refactoring"
would require a bit more: support for binding scopes beyond the current
buffer, treatment for derived names and notation (e.g. c vs. c_def vs.
funny syntax for c), and maybe some capture avoidance.


More information about the isabelle-dev mailing list