[isabelle-dev] Highlighting of locale variables
makarius at sketis.net
Fri Apr 12 15:24:07 CEST 2013
On Fri, 12 Apr 2013, Lars Noschinski wrote:
> I wonder whether it would be a good idea to distinguish the syntax
> highlighting for free variables and free variables fixed by a locale
> ("locale variables"). It seems that this information is already
> available to the IDE (these variables are marked as "fixed" when
Yes, I wanted to revisit that already for the last two releases, and make
the distinction of scopes even a bit more advanced.
> Rationale: In the locale context, these locale variables are morally
> constants. Somebody suggested to highlight locale variables like
> constants, but personally I'd prefer a highlighting similar to variables
> obtained or fixed in a proof (maybe a non-bold orange?).
Note that a "fixed variable" (funny name) is always like a "local
Can you point to situations where this is still treated differently?
Such incidents are mostly coming from the depths of time, as Larry usually
There are certain intermediate states, like undeclared frees that are
implicitly fixed by the system infrastructure via "auto fix", but that is
More information about the isabelle-dev