Email Gateway (Aug 22 2022 at 14:24): Email Gateway (Aug 22 2022 at 14:24):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
In Isabelle2016-1-RC2 the occurrences of P in "assumes" and "shows" are not highlighted and renamed:
theorem
fixes P
assumes P
shows P
proof -
show P using assms .
qed
theorem
P
proof -
show P sorry
qed
Relevant items in the NEWS file:
Highlighting of entity def/ref positions wrt. cursor.
Action "isabelle.select-entity" (shortcut CS+ENTER) selects all occurrences of the formal entity at the caret position. This facilitates systematic renaming.
Am I doing something wrong?
Thanks,
Jørgen
Email Gateway (Aug 22 2022 at 14:24):From: Makarius <makarius@sketis.net>
It is normal that PIDE markup is incomplete. Locale expressions and long
theorem statements don't have that yet, because the implementation has
too many features.
Another omission is markup for term bindings like ?thesis or those
stemming from let/is pattern matching.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC