RFR: JDK-6251738: Want a top-level summary page that itemizes all spec documents referenced from javadocs (OEM spec) [v3]

[Jonathan Gibbons]

> This introduces support for a new `@spec` tag that can be used as either an inline tag or as a block tag. It is used to identify references to external specifications, in such a way that the references can be collected together on a new summary page, called "Other Specifications", available from either the static INDEX page or the interactive search box.
> 
> As an inline tag, the format is `{@spec url label}`, which is roughly translated to `<a href="url">label</a>` in the generated docs.
> 
> As a block tag, the format is simply
> 
>     @spec url label
> 
> which is handled in a manner analogous to
> 
>     @see <a href="url">label</a>
> 
> The tag is notable for being the first standard/supported tag that can be used as either an inline or block tag. (We have had support for bimodal non-standard/custom tags for a while, such as `{@jls}` and `{@jvms}`.) To support bimodal standard tags, some changes to `DocCommentParser` are incorporated here.
> 
> This change is only the _support_ for the new tag;  it does _not_ include any changes to API docs to _use_ the new tag.

Jonathan Gibbons has updated the pull request with a new target base due to a merge or a rebase. The pull request now contains 12 commits:

 - Merge master
 - Fix merge issues; review feedback
 - Merge with master
 - allow rich content in createAnchorAndSearchIndex
 - update Docs.gmk to stop disabling spec tag
 - fix TestSpecTag.testEncodedURI
 - fix tests
 - remove support to workaround legacy @spec tag
 - Merge remote-tracking branch 'upstream/master' into new-spec-tag
 - fix trailing whitespace in test
 - ... and 2 more: https://git.openjdk.java.net/jdk/compare/300cbaa6...69595e04

-------------

Changes: https://git.openjdk.java.net/jdk/pull/790/files
 Webrev: https://webrevs.openjdk.java.net/?repo=jdk&pr=790&range=02
  Stats: 1374 lines in 42 files changed: 1337 ins; 14 del; 23 mod
  Patch: https://git.openjdk.java.net/jdk/pull/790.diff
  Fetch: git fetch https://git.openjdk.java.net/jdk pull/790/head:pull/790

PR: https://git.openjdk.java.net/jdk/pull/790