Strange, I get the same entities in the html code with greek (or German/Spanish/etc.) characters both in- and outside <pre><code></code></pre> blocks.
(Anyway, as I said, I like your patch. I think that making that change in the core would be good.)
(Anyway, as I said, I like your patch. I think that making that change in the core would be good.)