// requires jQuery (of course)
sS jsReplaceDivWithClass(S className, S html) {
  ret "$(" + jsQuote("." + className) + ").html(" + jsQuote(html) + ");";
}