sS js_replaceBodyContents(S html) {
  ret replaceDollarVars_js([[
    (function() {
      var target = document.querySelector("body");
      target.innerHTML = $html;
      nodeScriptReplace(target);
    })(); ]], +html);
}