Introduce Zoom control
In #3672, the broken zoom control in the Eclipse toolbar has been removed. (CTRL + Mousewheel continues to work).
For the new editors, an alternative way to set the zoom level via the UI should be offered. See e.g. attached screenshot of GIMP zoom control menu entries for an inspiration (this is certainly a superset of the functionality that we need in the first place).
(from redmine: issue id 3843, created on 2019-10-09)
- Relations:
- relates #3815 (closed)
- Uploads:
