Increase the height of bracket selection by one point

[ShahzaibIbrahim]

In some zoom level the highlight is too close to the text and cutoff sometimes.

Example:

Here with zoom 175% the bracket selection seems to cut off the text.

After increasing the size by 1 pt, we get something like this

To me this looks much more cleaner than the current state.

[github-actions]

Test Results

 2 972 files   -  45   2 972 suites   - 45   2h 30m 24s ⏱️ + 21m 6s
 8 230 tests ±  0   7 982 ✅ ± 0  248 💤 ± 0  0 ❌ ±0 
23 351 runs   - 149  22 616 ✅  - 94  735 💤  - 55  0 ❌ ±0 

Results for commit bd4c7a7. ± Comparison against base commit 0badc89.

♻️ This comment has been updated with latest results.

[vogella]

LGTM

[vogella]

@HeikoKlare any concerns here?

[laeubi]

Yes the -1 does not make any sense here.

[HeikoKlare]

This PR misses the mentioned that it is an extract of #3597, which combined two issues:

• The highlight not properly being scaled on higher zooms (which is the reason for the float-based Rectangle
• The highlight drawn on top of the bracket, caused by the -1.

While the first change is fine for me, I proposed to extract out the second change (removing the "-1") into a separate PR (see #3597 (comment)), as the "-1" was there to fit the highlight into the line (see screenshot here #3597 (review)). So there seems to habe been a specific reason for the -1 and it might be up for discussion if that should be removed (i. i.e., if the highlight should fit in the line or if highlight should not being drawn over the bottom part of the bracket).

And the PR description actually seems wrong, as the example with the bracket exceeding the highlight at some zooms is about the OfFloat change, which is already covered by that other PR. The screenshot of the result is a combination of the two changes instead of just the single one that is supposed to be done by this PR (putting the "-1" removal on top. @ShahzaibIbrahim can you please update this PR accordingly?

If I am not mistaken, this change on top of https://github.com/eclipse-platform/eclipse.platform.ui/pull/3597/files will just change this appearance:

with this:

[ShahzaibIbrahim]

Sorry, I failed to mention that this PR depends on #3597 before being review (to avoid conflicts). I will update the screenshots as well.

[HeikoKlare]

Yes the -1 does not make any sense here.

@laeubi I guess your change request (#3653 (review)) is obsolete since the PR now exactly removes the -1.