[isabelle-dev] Highlighting of locale variables

[Lars Noschinski]

On 12.04.2013 15:24, Makarius wrote:
> On Fri, 12 Apr 2013, Lars Noschinski wrote:
>> 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?).
[...]
> 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.

I was referring to variable fixed by a locale. In the example below, "F" 
is always rendered like a free variable (i.e. blue); although it's scope 
is not the lemma, but the locale.

-----------
locale dummy = fixes F :: 'a
begin

lemma "P F"
oops
-----------

> There are certain intermediate states, like undeclared frees that are
> implicitly fixed by the system infrastructure via "auto fix", but that
> is slightly different.

An oddity related to this is the let command. In the example below, "a" 
is rendered as an undeclared free. This feels wrong as writing such a 
statement seems perfectly fine, because constants and variables on the 
left hand side are generalized anyway.

-----------
notepad begin
   let "?X a" = "1 + a"
end
-----------

   -- Lars