Re: [isabelle] Issue with "try" and auto-indentation
On 30/10/16 09:00, Eugene W. Stark wrote:
> 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.
Thanks for keeping an eye on such fine points. I have changed that in
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and