Re: [isabelle] Systematic renaming



On 21/11/16 01:07, Jørgen Villadsen wrote:
> 
> 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.

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.