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 (it is updated in approx. 14 hours, at 1
am local time).


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