Re: [isabelle] the sound of a sledgehammer

I certainly hope instead to see a restoration of one of sledgehammer's key advantages, namely that it ran in the background so that you could indeed continue to work on your proof. This was one of its design goals from the very beginning.

The entire internal architecture supports this background execution, so it should be possible.

Larry Paulson

On 14 Feb 2013, at 11:40, John Wickerson <jpw48 at> wrote:

> Dear Isabelle,
> Following on from a point Tobias made a while ago, that ...
>> jedit ... forces you to wait until sledgehammer has returned before you can scroll around - otherwise s/h is interrupted and restarts
> ... can I suggest a new feature: that sledgehammer gives some sort of audible feedback? Because I can't do anything until the sledgehammer is finished, I usually type "sledgehammer", then go and browse the internet or look out of my window for a minute or so, then come back and see if it worked. So, I think it would be nice if sledgehammer made some sort of noise to tell me when it has succeeded or timed-out.
> John

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