++ commentLevel;
		    state = 3;
		} else if (c == ')') {
		    -- commentLevel;
		    state = commentLevel == 0 ? 0 : 3;
		} else if (c == '\\') {
		    state = 4;
		} else { state = 3;
		}
		break;
		// In a comment, backslash seen
		case 4:
		    if (myCurrentIndex >= mySourceLength) {
			myLexemeType = ILLEGAL_LEXEME;
			myLexemeBeginIndex = mySourceLength;
			myLexemeEndIndex = mySourceLength;
			state = -1;
		    } else {
			++ myCurrentIndex;
			state = 3;
		    }
		    break;
		    // In a token
		case 5:
		    if (myCurrentIndex >= mySourceLength) {
			myLexemeEndIndex = myCurrentIndex;
			state = -1;
		    } else if (Character.isWhitespace
			       (c = mySource.charAt (myCurrentIndex ++))) {
			myLexemeEndIndex = myCurrentIndex - 1;
			state = -1;
		    } else if (c == '\"' || c == '(' || c == '/' ||
			       c == ';'  || c == '=' || c == ')' ||
			       c == '<' || c == '>'  || c == '@' ||
			       c == ',' || c == ':' || c == '\\' ||
			       c == '[' || c == ']' || c == '?') {
			-- myCurrentIndex;
			myLexemeEndIndex = myCurrentIndex;
			state = -1;
		    } else {
			state = 5;
		    }
		    break;
		}
	    }
	    
	}
	
    }

    /**
     * Returns a lowercase version of the given string. The lowercase version  
     * is constructed by applying Character.toLowerCase() to each character of
     * the given string, which maps characters to lowercase using the rules of 
     * Unicode. This mapping is the same regardless of locale, whereas the 
     * mapping of String.toLowerCase() may be different depending on the  
     * default locale. 
     */
    private static String toUnicodeLowerCase(String s) {
	int n = s.length();
	char[] result = new char [n];
	for (int i = 0; i < n; ++ i) {
	    result[i] = Character.toLowerCase (s.charAt (i));
	}
	return new String (result);
    }

    /**
     * Returns a version of the given string with backslashes removed.
     */
    private static String removeBackslashes(String s) {
	int n = s.length();
	char[] result = new char [n];
	int i;
	int j = 0;
	char c;
	for (i = 0; i < n; ++ i) {
	    c = s.charAt (i);
	    if (c == '\\') {
		c = s.charAt (++ i);
	    }
	    result[j++] = c;
	}
	return new String (result, 0, j);
    }

    /**
     * Returns a version of the string surrounded by quotes and with interior
     * quotes preceded by a backslash.
     */
    private static String addQuotes(String s) {
	int n = s.length();
	int i;
	char c;
	StringBuffer result = new StringBuffer (n+2);
	result.append ('\"');
	for (i = 0; i < n; ++ i) {
	    c = s.charAt (i);
	    if (c == '\"') {
		result.append ('\\');