Re: [isabelle] Isabelle2013-1-RC1 available for testing
On Tue, 8 Oct 2013, Christian Sternagel wrote:
I find that on my machine (running the notorious 64bit Fedora 19 with
Gnome) when using the Sledgehammer panel, very often (it feels like the
majority of cases) after clicking "Apply", "Cancel" has no effect (the
whole buffer is grayish highlighted).
This should be different in Isabelle2013-1-RC2, and hopefully better.
In such cases sometimes clicking "Apply" again actually cancels the
ATPs, but sometimes only restarting Isabelle/jEdit helps (or maybe I
would have to wait longer than 1 minute).
In such cases of uncertainty I merely reload the current buffer (F5),
which is normallly sufficient. This operation is somehow reminiscent of
proof-tract-buffer in Proof General :-)
For sledgehammer in particular, the "interaction state" is tied to the
syntactic command span in the text. So if that is edited or removed any
associated operations on the prover side should be canceled. The "Locate"
button reveals the command that is associated with the current query
This archive was generated by a fusion of
Pipermail (Mailman edition) and