[isabelle] Issue with "try" and auto-indentation



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




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