[isabelle-dev] JEdit: type constraints no longer printed by default

[Makarius]

On Thu, 10 Jan 2013, Steffen Juilf Smolka wrote:

> Is this the intended behaviour? It used to be different a couple of 
> month ago. I don't know when it changed exacyly, but I think changeset 
> a6814de45b69 might be responsible for the change.

Yes, that change is in the vicinity where I was working on show_markup. 
See 1301ed115729 for the first occurrence of the corresponding 
documentation.

So with show_markup enabled, type and sort constraints are moved from the 
text to the markup over the text.  This all works surprisingly well for 
what it does -- it was considered impossible to do such things a few years 
ago.

There might be corner cases where the change of the display leads to odd 
effects.  Are there concrete incidents already that need to be 
reconsidered before the release?


 	Makarius