ROOTS

less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
propagate flush from ML to Scala via special protocol message;
more formal type Message_Channel.message;

src/Pure
src/FOL
src/HOL
src/ZF
src/CCL
src/CTT
src/Cube
src/FOLP
src/LCF
src/Sequents
src/Doc