DDOC_PSYMBOL = <a name="$0"></a><span style="color:OrangeRed" class="ddoc_psymbol">$0</span>
DDOC_PSUPER_SYMBOL = <a name="$0"></a><span style="color:blue" class="ddoc_psuper_symbol">$0</span>