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

[Makarius]

On Tue, 19 Apr 2016, Dmitriy Traytel 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).

I have already reworked other packages (definition, inductive, function) 
to pin the markup more to the point, although a bit of internal 
implementation details are still exposed occasionally.

For example, the derived_name operations in 
http://isabelle.in.tum.de/repos/isabelle/annotate/d743bb1b6c23/src/HOL/Tools/Function/function_lib.ML#l41 
remove position information for derived fact names etc. 
Thm.make_def_binding is similar for plain definitions done internally.

Concerning datatype, see also these hints about mixfix annotations: 
http://www.mail-archive.com/isabelle-dev%40mailbroy.informatik.tu-muenchen.de/msg06765.html


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".

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


 	Makarius