[isabelle-dev] Highlighting of locale variables

Makarius 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 
> hovering).

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 
constant".

Can you point to situations where this is still treated differently? 
Such incidents are mostly coming from the depths of time, as Larry usually 
calls this.

There are certain intermediate states, like undeclared frees that are 
implicitly fixed by the system infrastructure via "auto fix", but that is 
slightly different.


 	Makarius



More information about the isabelle-dev mailing list