static void mreplace(Matcher m, StringBuffer buf, S s) {
  m.appendReplacement(buf, Matcher.quoteReplacement(s));
}