Changed printing of symbols.

Added a PPRINT-XHTML-SYMBOL in order to print only the symbol name, thus
avoiding messing up with the symbol package.
It may have to be fixed in the future by adding a knob.