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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
