[isabelle-dev] JEdit: type constraints no longer printed by default
makarius at sketis.net
Fri Jan 11 12:38:42 CET 2013
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
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
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?
More information about the isabelle-dev