3 class WhiteSpace extends InputElement {
5 WhiteSpace(char which) {
9 public String toString() {
12 case ' ': s = "SP"; break;
14 case '\t': s = "HT"; break;
16 case '\f': s = "FF"; break;
18 case '\n': s = "LT"; break;
20 default: s = "Unknown Whitespace character."; break;
22 return "Whitespace <"+s+">";