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

[Steffen Juilf Smolka]

> 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?

We use Syntax.string_of_term when creating Isar proof scripts in Sledgehammer and rely on Type.contstraint to introduce type annotations in terms (this does not work with show_markup set to true).

Also, we got the error "Malformed YXML: multiple results" in certain situations.

Both problems are solved as of 0583db803066, simply by setting show_markup to false in Sledgehammer.

Steffen