[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

> * If sledgehammer (both over panel and as command) is running, further
> processing of the file is blocked/very slow. Thus, it is not possible
> to run sledgehammer and, in parallel, continue exploration to find your
> own proof. In PG, parallel sledgehammering works, and I used it
> extensively. In Isabelle/jEdit I now think twice before I invoke
> sledgehammer, because it just interrupts my workflow and I have to wait
> for it to finish staring at the sledgehammer-window and doing nothing.

This sounds like some serious performance problem, and requires proper 
reports on your hardware and system parameters.

In Isabelle2014 the Sledgehammer integration is in its third generation. 
It is supposed to work without problems.


 	Makarius