private String readText() throws IOException {
      StringBuilder sb = new StringBuilder();
      int ch = in.read();
      while (!isWhiteSpace(ch) && !isLeftParen(ch) && !isRightParen(ch)) {
        sb.append((char) ch);
        ch = in.read();
      }
      in.unread(ch);
//      System.out.println("Read text: ["+sb+"]");
      return sb.toString().intern();
    }