prettyprint.js

(function() {
    try {
        prettyPrint();
    } catch(e) {
        var scriptId = 'prettyPrinter';
        if (document.getElementById(scriptId) === null) {
            var elem = document.createElement('SCRIPT');
            elem.id = scriptId;
            elem.onload = function() {
                prettyPrint();
            }
            elem.src = "https://google-code-prettify.googlecode.com/svn/trunk/src/prettify.js";
            var theBody = document.getElementsByTagName('body')[0];
            theBody.appendChild(elem);
        }
    }
})();