Email Gateway (Aug 22 2022 at 16:22): Email Gateway (Aug 22 2022 at 16:22):From: Peter Lammich <lammich@in.tum.de>
Hi all,
I always thought that the feature "Select all occurrences of formal
entity at caret" (CS+ENTER by default) was intended to easily rename
all occurrences of, e.g., a constant, and it was very useful for me in
the past.
I now ran into the following problem:
It also will select the mixfix syntax referring to the constant,
and typing in a new name does not yield the desired result in this
case, as it replaces the mixfix syntax naively with a new name.
Is there a possibility to only select literal occurrences of an
entity?
Email Gateway (Aug 22 2022 at 16:23):From: Makarius <makarius@sketis.net>
No, I don't know a better way right now.
The documentation of isabelle.select-entity is very careful to say it
"facilitates systematic renaming", without any claims that it works
under all circumstances.
Strictly speaking, there is a mismatch of concepts here: markup for
formal entities does not care about the syntactic appearance in the
text: it could differ wrt. quotes, name space prefixes, mixfix syntax etc.
Actual first-class "refactoring" of names seen in the source would
require a different approach at the bottom of it.
Makarius
Email Gateway (Aug 22 2022 at 16:23):From: Dominique Unruh <unruh@ut.ee>
One hack for solving your problem is the following:
- Select occurrences of my_Ex using CS-Enter
- Open find with Ctrl-F
- Type my_Ex and your_Ex into search and replace fields
- Make sure "Search in: Selection" is checked (I think it is by default).
- Alt-A for "Replace All"
This will replace only within the selection from CS-Enter, but will also
only replace the literal string, not the syntactic sugar (unless you have a
very exotic syntax).
Of course, it would be nice if this were automated, but I think it's still
quite OK for occasional refactorings.
Best wishes,
Dominique.
Last updated: Nov 21 2024 at 12:39 UTC