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
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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.