docs: private static String reduceStringLiteralToken(String image) {
      // First, remove leading and trailing ' character
      image = image.substring(1, image.length()-1);
      // Next, de-double any doubled occurances of the ' character
      for (int i = 0; i < image.length(); i++)
        if (image.charAt(i) == '\'')
          // Here's a ', which we retain, but the character after it, also a ', is elided
          image = image.substring(0,i+1) + image.substring(i+2);
      return image;
    }