What could be the reason that deprecated symbols are not marked as usual in
#9920? The "Deprecated symbol" in the Java Colors & Fonts section has a
check box at Error Stripe Mark and Effects, but my file shows a green square
at the top right corner.
Thanks in advance,