diff options
| author | Hugo Herbelin | 2019-09-11 10:26:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-13 14:35:07 +0200 |
| commit | b7a9d3e02b01124179f5a9cdf217a4f4f13d8c24 (patch) | |
| tree | 762d39fc7f4caebddfb32bb4388ed0200b84671b /plugins | |
| parent | 4debcab8771f0c2f52b7697dbf2233f931f863e6 (diff) | |
Hack for fixing #10578 (wrong initial handle position separating main windows).
G. Melquiond noticed that the size_allocate event is emitted in the
Layout step of the Events-Update-Layout-Paint gtk+ loop so that it is
actually processed only when a further event arrived. In some
circonstances, this next event has to be an action from the user. So,
in some circonstances, at initialization of Coqide, the handle, whose
positioning was precisely governed by the size_allocate event, was
only set at its expected position after a first action of the
user. Before this first action of the user, the handle separating the
buffer and the pair of goal and message windows, as well as the handle
separating the goal window and the message window were located in the
leftmost uppermost corner, which gave an impression of non-usability
of CoqIDE.
To prevent this, we early set the position of the handle at an
estimated value depending on the width and height of the whole coqide
windows in the preferences.
(Also removing a previous temporary setting of the handle position to
- strangely - value 1 but this was anyway overwritten by the
size_allocate event.)
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions
