explicit message_output thread, with flushing after timeout, ensure atomic user-operations without the danger of IO Interrupt; eliminated auto_flush threads -- use plain line buffering for stdout/stderr; tuned;

more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

explicitly qualify type Output.output, which is a slightly odd internal feature;

export main ML entry by default; observe elisp format for preferences; clarified command setup;

observe Isabelle/ML coding standards;

merged

significantly improved Isabelle/Isar implementation manual;