Correctly escape Javadoc code snippets

Escaping code snippets for use in Javadoc comments is non-trivial. By default,
Javadoc comments are expected to be HTML markup. While HTML offers `<pre>` and
`<code>` tags, these only handle formatting and do not remove the need to escape
e.g. characters such as `<` and `>`. To this end, Javadoc provides options such
as `{@code ...}` for embedding text verbatim. However, these only handle
escaping and not formatting. One thus generally combines the two approaches to
yield comments like `<pre>{@code ...}</pre>`. However, *this* combination itself
introduces challenges around escaping:

* `@`, which normally indicates a Javadoc tag (such as `@code` itself), needs to
  be escaped in some situations but not others:

```java
/**
 * <pre>
 * {@code
 * public class C {
 *   // This use of @ needs to be escaped lest Javadoc get confused and think
 *   // it's a nested tag (even though @code should explicitly prevent this).
 *   @SuppressWarnings
 *   public static void m1() {}
 *
 *   // This @ does not need to be escaped.
 *   public static void m2() {}
 * }
 * }
 * </pre>
 */
```

* Braces (`{` and `}`) need to be escaped if they are not balanced, since
  Javadoc counts braces in order to work out when to end the `@code` block.
* The combination `*/` always needs to be escaped since it would otherwise
  premutately terminate the Javadoc comment.

Our escaping code is currently broken (see #1363), causing crashes because it
fails to handle the case of unbalanced braces. Even in the cases where it does
not cause crashes, the Javadoc generated is not necessarily faithful to the
input, due to incorrect escaping of `@` and `*/` depending on the context. For
instance, while many sources state that `{@literal @}` is the correct escaping
of `@` within a `@code` block, this is not in general true and will result in
`{@literal @}` being produced in the rendered output instead of the desired `@`.

This commit attempts to fix it once and for all. We do this by adopting a
strategy whereby we leave the `@code` block temporarily when the need to escape
a character arises. For example, given:

```java
This contains an @ and {unbalanced braces
```

we now generate:

```java
This contains an }{@literal @}{@code  and }{{@code unbalanced braces
```

with the expectation that this will end up inside a `<pre>{@code ...}</pre>`
context. This results in generated comments that are harder to read, but render
successfully and accurately, both as HTML Javadoc pages and e.g. hover
documentation in most IDEs. The test suite for Javadoc processing has been
bulked out so that hopefully this does not bite again (famous last words!).

Fixes #1363

CHANGELOG_PENDING.md

@@ -3,3 +3,4 @@
 
 ### Bug Fixes
 
+- Correctly escape special characters in generated Javadocs.