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

[Hannes Wallnöfer]

On Thu, 27 Apr 2023 12:50:07 GMT, Hannes Wallnöfer <hannesw at openjdk.org> wrote:

> 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.

This pull request has now been integrated.

Changeset: 52ec4bcb
Author:    Hannes Wallnöfer <hannesw at openjdk.org>
URL:       https://git.openjdk.org/jdk/commit/52ec4bcb1bab15dbf0a9b2488d33a23cdc1cb0e1
Stats:     125 lines in 5 files changed: 106 ins; 4 del; 15 mod

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

Reviewed-by: jjg

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

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