// drop only /* */ comments
sS tok_javaDropSlashStarCommentsFromWhitespace(S s) {
  int l = l(s), j = 0;
  new StringBuilder buf;
  while (j < l) {
    int i = j;
    char c = s.charAt(j);
    char d = j+1 >= l ? '\0' : s.charAt(j+1);
    if (c == '/' && d == '*') {
      do ++j; while (j < l && !s.substring(j, Math.min(j+2, l)).equals("*/"));
      j = Math.min(j+2, l);
    } else if (c == '/' && d == '/') {
      do ++j; while (j < l && "\r\n".indexOf(s.charAt(j)) < 0);
      buf.append(substring(s, i, j)); // keep comment
    } else {
      buf.append(c); ++j;
    }
  }
  ret str(buf);
}

Began life as a copy of #1008628