As pointed out by @thunderhook in the review of #3543 it would be good if we can change the usage of <code> in the Javadoc to <code class='java'> where it makes sense to improve how it looks like in IntelliJ.