proper startup for Pure: its use_prelude produces stdout before stderr protocol init;

proper context for loading Pure;

clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";

close socket explicitly (idempotent);

more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);

simplified code and proofs

automated proof

merged

cleaned proofs

clarified signature;