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

[Makarius]

On Fri, 11 Jan 2013, Steffen Juilf Smolka wrote:

> 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).

Yes, it is correct to set show_markup=false in the context before 
printing.  Note that this is not specific to jedit, but to Isabelle in 
general.  It is just an accident that jedit is right now the only 
application that enables show_markup routinely.


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

In which situations?  Do you have an exception trace?  The message is from 
YXML.parse, but in most situations one has YXML.parse_body anyway.  And in 
fact, user code should hardly ever come across anything here, at least in 
theory.


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

BTW, just formally your data (diff over source) and meta-data (log entry) 
in the changeset have quite an overlap, close to being a parrot.

You should not put historical explanation into the source -- it becomes 
outdated rather quickly and make the text unreadable. The point where you 
explain what you think you did is the log.


 	Makarius