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
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