[isabelle-dev] Highlighting of locale variables

Lars Noschinski noschinl at in.tum.de
Fri Apr 12 14:35:03 CEST 2013


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

More information about the isabelle-dev mailing list