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?).
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
