[isabelle] the sound of a sledgehammer



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.