[isabelle] the sound of a sledgehammer
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and