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