[isabelle-dev] Highlighting of locale variables

[Lars Noschinski]

Hi,

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

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?).