Java/AWT/Swing problem with text input boxes vs. mouse selection

[Makarius]

The Isabelle/jEdit documentation now (Isabelle/e761a9aff49b) has this new 
snippet in chapter "Known problems and workarounds":

   ▪ ❙‹Problem:› On macOS, text input boxes may get into a bad state, where all
   text is selected, but further editing only replaces that by the next input
   character. This often happens, after selecting all text with the mouse from
   the ∗‹right›.

   ❙‹Workaround:› Select text with the mouse from the ∗‹left›, or use regular
   keyboard shortcuts like ▩‹C+a› or ▩‹S+HOME›.

Despite a lot of time spent on investigations, I can do nothing about it. The 
problem belongs to the OpenJDK project. Here are notable tickets:

   * https://bugs.openjdk.org/browse/JDK-8325052 (Jan-2024,closed)
   * https://bugs.openjdk.org/browse/JDK-8319880 (Nov-2023, open)

We can merely wait a few more years, until they finally close that.

Interestingly, the problem can be even seen in IntelliJ IDEA, despite all its 
ambitious add-ons to the GUI, and so many Java experts using it every day.


	Makarius