aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
authorHugo Herbelin2019-09-11 10:26:37 +0200
committerHugo Herbelin2019-09-13 14:35:07 +0200
commitb7a9d3e02b01124179f5a9cdf217a4f4f13d8c24 (patch)
tree762d39fc7f4caebddfb32bb4388ed0200b84671b /plugins
parent4debcab8771f0c2f52b7697dbf2233f931f863e6 (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