[POC] When computing the size of a widget always return values rounded up #2502
+34
−8
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
When converting pixels to point there can be depending on the zoom level be a fractional result. Currently in all cases these result is converted into an integer using `Math.round()` that will make values `+/-0.5` resulting in small values to be round towards a smaller value. While it is maybe valid for a _location_, when using points to express a _dimension_ this is not okay as it will result in the reported (integer) value to be to small leading to errors when the SWT API is then used after performing additional computations maybe. This now makes the following adjustments: 1. Introduce a rounding mode that allows different ways of rounding and adds as a first step ROUND (the previous default) and UP (for always round towards the largest integer) 2. Adjust the `Control` class to decide what mode is best in what situation. See - eclipse-platform#2381 - eclipse-platform#2166
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
When converting pixels to point there can be depending on the zoom level be a fractional result.
Currently in all cases these result is converted into an integer using
Math.round()that will make values+/-0.5resulting in small values to be round towards a smaller value (see here).While it is maybe valid for a location, when using points to express a dimension this is not okay as it will result in the reported (integer) value to be to small leading to errors when the SWT API is then used after performing additional computations maybe.
This now makes the following adjustments:
Controlclass to decide what mode is best in what situation.See