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