Email Gateway (Aug 22 2022 at 14:13): Email Gateway (Aug 22 2022 at 14:13):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
In Isabelle2016-1-RC1, the new auto-indentation features interact
badly with "try" in the following sense: If I type "try" in the JEdit
buffer to invoke sledgehammer, and then I click on a proposed proof
method that comes up in the output window, then not only is the
proposed proof method inserted into the buffer, but the line with "try"
is re-indented, causing sledgehammer to be restarted instead of continuing
along to find additional possible proof methods.
Previously one could click on the proposed proof methods as they appeared
to capture them in the buffer for posterity without causing sledgehammer
to be restarted.
- Gene Stark
Email Gateway (Aug 22 2022 at 14:35):From: Makarius <makarius@sketis.net>
Thanks for keeping an eye on such fine points. I have changed that in
https://bitbucket.org/isabelle_project/isabelle-release/commits/f630e9385d7e03b6021616f2b00a82bd8c1b0489
so it should work better in the next release candidate.
You can also try it with the nightly snapshot from
http://isabelle.in.tum.de/devel (it is updated in approx. 14 hours, at 1
am local time).
Makarius
Last updated: Apr 26 2024 at 20:16 UTC