Taclet match dialog: readable \assumes candidates and smarter window placement

[unp1]

Intended Change

Two usability fixes to the redesigned taclet-match dialog.

1. Readable \assumes candidates in "Select from sequent" mode.
When picking (rather than typing) an \assumes instantiation, each candidate
sequent formula was rendered with only its first physical line. A formula that
the pretty-printer wraps across several lines therefore showed a short stub — or
nothing at all, when it began with a newline, followed by blank space, and it
abbreviated far too early. The candidate now flattens the whole formula onto one
line, and the abbreviation limit is raised from 100
to 200 characters so more of the formula is visible before the ellipsis. The
full formula remains available on hover.

2. Smarter window placement.
The dialog was centred over the main window (setLocationRelativeTo), so it
covered the sequent view, exactly what the user needs in order to read a
variable name or drag a sub-term onto a field. It now auto-places itself beside
the sequent view: to the right if there is room, else to the left, else docked
to the roomier screen edge, always fully on screen. Within a session it reuses
the last position the user moved it to. The position is intentionally not
persisted across restarts (where the main window may sit elsewhere, a stale
absolute position would be worse than a fresh placement); the window size is
still persisted as before.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality (TmTextTest.collapseToLine now covers wrapped-formula indentation and trimming).
• I have tested the feature as follows: :key.ui compiles and passes spotless; the de.uka.ilkd.key.gui.tacletmatch.* test suite is green. Manually verified that a multi-line \assumes candidate now reads as one line, and that the dialog opens beside the sequent view instead of on top of it (and reopens where it was last moved).
• I have checked that runtime performance has not deteriorated (pure UI/text change).

Additional information and contact(s)

Follow-up polish on top of the redesigned taclet-match dialog. Both changes are
confined to the de.uka.ilkd.key.gui.tacletmatch package.

Created with AI tooling support

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.