static S javaTok_substring(S s, int i, int j) {
  if (i == j) ret "";
  if (j == i+1 && s.charAt(i) == ' ') ret " ";
  ret s.substring(i, j);
}