Fix bugs in Sodium

tools/sodium/sodium.js

Index: tools/sodium/sodium.js
diff --git a/tools/sodium/sodium.js b/tools/sodium/sodium.js
index 44475a177f77151e6fddf78438ce03d899e71cc4..0d2eff55b43973ffb783b9a3611d8e374bac5779 100644
--- a/tools/sodium/sodium.js
+++ b/tools/sodium/sodium.js
@@ -342,9 +342,14 @@ var Sodium = (function() {
     var source = getCurrentSourceText();
     var sourceDivElement = document.getElementById('source-text');
     var code = getCurrentCodeObject();
-    var newHtml = "<pre class=\"prettyprint linenums\" id=\"source-text\">"
-      + 'function ' + code.name + source + "</pre>";
-    sourceDivElement.innerHTML = newHtml;
+
+    var new_pre = document.createElement("pre");
+    new_pre.classList.add('prettyprint');
+    new_pre.classList.add('linenums');
+    new_pre.id = 'source-text-pre';
+    new_pre.textContent = 'function ' + code.name + source;
+    sourceDivElement.replaceChild(new_pre, sourceDivElement.firstChild);
+
     try {
       // Wrap in try to work when offline.
       PR.prettyPrint();