[isabelle-dev] NEWS: Highlighting of entity def/ref positions

[Jasmin Blanchette]

Hi Dmitriy, Makarius,

Dmitriy wrote:

> At first I was a bit surprised to see the first occurrence of list, Nil, and Cons in blue in the following datatype definitions.
> 
> datatype 'a list = Nil | Cons 'a "'a list”
> 
> But I guess, it makes sense to indicate that this is a new thing being defined.
> 
> The question is whether the list on the right hand side of the above datatype should also be blue (as in fun the recursive occurrences are also blue). IIRC, we are doing some context tricks to make it look black (Jasmin knows better).

There is no concept in Isabelle for a free type constructor -- only for a type variable (e.g., 'a), which is nullary and must start with a quotation mark. Therefore, to parse things like "'a list" and "('a, 'b) rbt" on the right-hand side of the definition of these types, we must pass a fake context in which "list" and "rbt" are already declared as unary resp. binary type constructors. This explains the black color. I believe a similar trick was done by Berghofer-Wenzel, in their function "prep_specs" ("~~/src/HOL/Tools/Old_Datatype/old_datatype.ML").

Makarius wrote:

> At some point we could also revisit the color code for "free" variables. A local theory target has a notion of "hypothetical constant" that is defined first, and later founded as actual constant in the background. Instead of blue, it could be just shown black and reported as "hypothetical const" instead of "free variable".

Or you could go for dark blue, so that one gets a subtle (and sometimes useful) hint that one is referring to something being defined.

> The classic meaning of blue/free should probably be restricted to auto-fixed variables or explicit fixes of a toplevel statement.

I fully agree.

Jasmin