[jsr369-experts] Push API vJetty2: headers

From: Shing Wai Chan <shing.wai.chan_at_oracle.com>
Date: Fri, 21 Aug 2015 16:14:06 -0700

In PushBuilder, I notice there are several getters API?
Do we really need that?

If we decide to keep those APIs, then we need to take a closer look.
In PushBuilder, we have:
     Set<String> getHeaderNames()

Is the modification of the resulting Set has any effect on push request?
It should not. In this case, I suggest to add the following
clarification in the javadoc:

     Any changes to the returned Set must not affect the push request.

How can we handle the case of headers with the same header name?
As in HttpServletRequest, we would to like to add the following API:
     Collection<String> getHeaders(String name)

Shing Wai Chan