Replace calls to htmlspecialchars() with sm_encode_html_special_chars().

New function sm_encode_html_special_chars() encodes HTML special
characters by calling htmlspecialchars(). It sets the character set
to ISO-8859-1, to fix compatibility with PHP >= 5.4.

See #3491925