I've discovered another whitespace trimming issue with <pre> tags. By applying the test case given in ticket #346 in Internet Explorer:
<pre>
/***
* First line (above) is blank.
* Some more text...
*/
public void testFunction(){
System.out.println( "abc" );
}
</pre>
Switching between source and WYSIWYG mode after that, once, would delete the first line break. Switching again would delete the second line break.
After some experiments, the culprit to this problem is found to be the Microsoft.XmlDom ActiveX we're using to reassemble the document between mode switches. The xml property's value of this ActiveX object would chop exactly one newline character off from the beginning of the <pre> tag, if one can be found.