Make sure that large volumes of data can be handled by all parts of infrastructure

[David Aspinall]

This is the old problem of too much output "choking"

• In some cases we may want to prevent output going to interfaces at all
• Other cases we must decide that interface can cope, and consider how it should display

[Makarius]

After all these years living with the choking problem in Proof General, a rather trivial solution has shown up that works well for single-core (!) machines: the prover process is run with "nice", while the interface maintains full priority. When the latter is busy processing prover output, it automatically sucks CPU cycles from the prover, slowing it down considerable (say from 90% to 10% CPU time).

Too bad everybody has multi-core machines now :-(

[David Aspinall]

Milestone PG-Eclipse-1.1.0 deleted