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;