3 class WhiteSpace extends InputElement {
5 WhiteSpace(char which) { this.whitespace=which; }
7 public String toString() {
10 case ' ': s = "SP"; break;
11 case '\t': s = "HT"; break;
12 case '\f': s = "FF"; break;
13 case '\n': s = "LT"; break;
14 default: s = "Unknown Whitespace character."; break;
16 return "Whitespace <"+s+">";