Re: [isabelle] the sound of a sledgehammer

On Thu, 14 Feb 2013, John Wickerson wrote:

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.

The JVM might support sound and more, but I don't know how it works out in practice. JavaFX might be another starting point for multi-media etc.

I am myself not as ambitious right now. For Isabelle2013 I have dared to use pupup windows with a little bit of focus change, and it caused a lot of trouble that is not fully settled yet (e.g. with strange Linux window managers).

Generally note that the synchronous behaviour of sledgehammer in Isabelle/jEdit is accidental. The documement model is meant to be as asynchronous and parallel as feasible, so you don't wait in the first place. Having 5 sledgehammers in parallel would also cause a lot of noise if they would produce audible feedback.

I had already sketched an approach to integrate "asynchronous agents" natively into the document model around 2009, but got distracted by endless other problems, like maintaining Proof General at the same time, people asking for imitation of Proof General features in Isabelle/jEdit, Oracle and Apple fighting each other etc.

After stopping Proof General maintenance in October 2011, progress with Isabelle/jEdit has become much faster. And I hope to have a chance to revisit the old "asynchronous agents" idea soon, if there are not again all these distractions and complaints about things changing.


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