Support extracting javadoc HTML files generated by Javadoc 17

[GorgiAstro]

Java 17 breaks the javadoc HTML file format again...

This proposal adds support for extracting HTML files generated by javadoc 17.

However, there is one bug that I didn't manage to fix after several hours of debugging: with javadoc 17 HTML files, there is a whitespace wrongly trimmed between public class and the name of the class. For instance, public class OpenIntToFieldHashMap is wrongly transformed to public classOpenIntToFieldHashMap.

I attached a ZIP file containing two HTML javadoc files from the same java code, one exported with java 11, one with java 17. However, I didn't check the backwards compatibility with java 8 and 14 for instance, I only checked with Java 11 and 17.

example_html_javadoc_11_vs_17.zip