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