Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] JEdit: type constraints no longer printed by default
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
[isabelle-dev] JEdit: type constraints no longer printed by default
In af8ecf09a58c, type constraints are no longer printed by default in JEdit:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term @{context}
| writeln
*}
# f
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.
When setting show_markup to false, the behaviour is like it was in the past:
ML {*
@{term f}
| Type.constraint @{typ nat = nat}
| Syntax.string_of_term (@{context} | Config.put show_markup false)
| writeln
*}
# f∷nat ⇒ nat
Regards,
Steffen___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
