sS tok_escapeStars(S s) {
  ret join(replace(javaTok(s), "*", "\\*"));
}