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

[Dmitriy Traytel]

Hi Makarius,

this is nice. 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).

Dmitriy


> On 18 Apr 2016, at 16:24, Makarius <makarius at sketis.net> wrote:
> 
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> 
> * Highlighting of entity def/ref positions wrt. cursor.
> 
> 
> This refers to Isabelle/15e6ae52e91a, where it is pushed through most definitional packages already.
> 
> Name bindings need to be treated carefully with their position information, but it also needs to be reset in certain situations (typically for derived fact names).
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev