ソースを色付けするブックマークレット

ソースを色付けするGreasemonkeyスクリプト - ヒルズで働く@robarioの技ログ
上記はボタン押下で動作するようになっている。
ブックマークレットならいきなり動作すればよいので書き換え。
長いので IE では動きません。*1

javascript:(function(d,s,h){if(!d.doctype){h='<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"><html><head><script type="text/javascript" charset="utf-8" src="'+s+'"></script><style type="text/css">pre.prettyprint{background:white;color:black}.str{color:maroon}.kwd{color:teal}.com{color:green}.typ{color:olive}.lit{color:silver}.pun{color:black}.pln{color:black}.tag{color:purple}.atn{color:teal}.atv{color:maroon}.dec{color:purple}</style></head><body onload="prettyPrint()"><pre class="prettyprint">'+d.body.innerHTML.replace(/<\/?pre>/ig,'')+'</pre></body></html>';d.open('text/html','replace');d.write(h);d.close()}})(document,'http://holidays-l.googlecode.com/svn/trunk/gm_scripts/prettify.js')

*1:外部ファイルにするのさぼっただけ。