tuned settings;

merged

removed references to OldTerm.*

tuned message_text;

removed obsolete XML mode; tuned comments; tuned;

xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;

Markup.no_output;