Hi,
I feel that http://wiki.phpmyadmin.net/pma/Gettext_for_developers should mention something about whether it is useful/needed to run the output of __('Default') through htmlspecialchars.
To the best of my knowledge this is not needed, and just adds overhead. But a quick grep in the code pointed me to 23 lines doing this.
Please correct me if I'm wrong here...Michal?