RFR: JDK-8303056: Improve support for Unicode characters and digits in JavaDoc search

[Hannes Wallnöfer]

Please review a change to make JavaDoc search Unicode-aware and better handle elements and index items with digits in their names. The most significant change is to use Unicode property escapes in regular expressions in the search script, but a few other changes were needed. In addition to running the updated test I did extensive manual testing on multiple desktop and mobile browsers to make sure search behavior did not change for other cases.

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

Commit messages:
 - JDK-8303056: Improve support for Unicode characters and digits in JavaDoc search

Changes: https://git.openjdk.org/jdk/pull/13690/files
 Webrev: https://webrevs.openjdk.org/?repo=jdk&pr=13690&range=00
  Issue: https://bugs.openjdk.org/browse/JDK-8303056
  Stats: 125 lines in 5 files changed: 106 ins; 4 del; 15 mod
  Patch: https://git.openjdk.org/jdk/pull/13690.diff
  Fetch: git fetch https://git.openjdk.org/jdk.git pull/13690/head:pull/13690

PR: https://git.openjdk.org/jdk/pull/13690