clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9);