WordPress: Smilies für vorformattierten Text deaktivieren

Der JavaScript Syntax-Highlighter SyntaxHighlighter ist mittlerweile recht bekannt und auch als Plugin für WordPress verfügbar. Leider ist nun so, dass bestimmte Zeichen in einem Quellcode – z.B. 8); – zu einem Smiley konvertiert werden.
Das sorgt dafür, dass die Smilies den kompletten Quellcode zerstören. Für die Umwandlung von Sonderzeichen sorgt die Funktion wp-includes/formatting.php/convert_smilies($text).

Mit folgendem Code (WP 2.7.1, ab Zeile 1094) werden vorformattierte Texte – d.h. die mit <pre> eingeleitet werden – nicht mehr mit Smilies verunreinigt:

/**
* Convert text equivalent of smilies to images.
*
* Will only convert smilies if the option 'use_smilies' is true and the globals
* used in the function aren't empty.
*
* @since 0.71
* @uses $wp_smiliessearch, $wp_smiliesreplace Smiley replacement arrays.
*
* @param string $text Content to convert smilies from text.
* @return string Converted content with text smilies replaced with images. Pre-formatted text is ignored.
*/
function convert_smilies($text) {
  global $wp_smiliessearch, $wp_smiliesreplace, $post;
  $output = '';

  if ( get_option('use_smilies') && !empty($wp_smiliessearch) && !empty($wp_smiliesreplace) ) {
    // HTML loop taken from texturize function, could possible be consolidated
    $textarr = preg_split("/(<.*>)/U", $text, -1, PREG_SPLIT_DELIM_CAPTURE);
    // capture the tags as well as in between
    $stop = count($textarr);// loop stuff

    $bInPreFormattedText = FALSE;

    for ($i = 0; $i < $stop; $i++) {
      $content = $textarr[$i];

      // pre-formatted text reached => set flag
      if (strpos($content, "<pre") !== FALSE) {
        $bInPreFormattedText = TRUE;
      }

      // pre-formatted text ends => disable flag
      if (strpos($content, "</pre>") !== FALSE) {
        $bInPreFormattedText = FALSE;
      }

      if ((strlen($content) > 0) && ('<' != $content{0}) && !$bInPreFormattedText) {
        // If it's not a tag and we are not in an <pre>-tag
        $content = preg_replace($wp_smiliessearch, $wp_smiliesreplace, $content);
      }

      $output .= $content;
    }
  } else {
    // return default text.
    $output = $text;
  }

  return $output;
}