Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Formal entity renaming (via CS+Enter) messing ...


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC