[isabelle-dev] Highlighting of locale variables
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