diff options
| author | Guillaume Melquiond | 2019-11-07 19:14:44 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2019-11-07 19:14:44 +0100 |
| commit | 882e37cfa843ff7444525550e7ac3fe44b1fcecb (patch) | |
| tree | 6eff644df6493ec227cecda1b01504203ab5aab0 /ide/session.ml | |
| parent | 64ddd9ac0c34e560a0640297e2e23b6aaf074810 (diff) | |
Do not rely on the user settings but on the actual window size. (Fixes #10956)
This should fix the issue when creating new session panes. The initial
session panes, however, might still be wrongly sized, as we do not yet
know, at the time they are created, if the window manager will respect the
user settings fixing the window size.
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/session.ml b/ide/session.ml index 38fdd0ef2a..2824530c43 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -432,6 +432,8 @@ let kill (sn:session) = sn.script#destroy (); Coq.close_coqtop sn.coqtop +let window_size = ref (window_width#get, window_height#get) + let build_layout (sn:session) = let session_paned = GPack.paned `VERTICAL () in let session_box = @@ -514,9 +516,9 @@ let build_layout (sn:session) = iteration of the loop *) let () = (* 14 is the estimated size for vertical borders *) - let estimated_vertical_handle_position = (window_width#get - 14) / 2 in + let estimated_vertical_handle_position = (fst !window_size - 14) / 2 in (* 169 is the estimated size for menus, command line, horizontal border *) - let estimated_horizontal_handle_position = (window_height#get - 169) / 2 in + let estimated_horizontal_handle_position = (snd !window_size - 169) / 2 in if estimated_vertical_handle_position > 0 then eval_paned#set_position estimated_vertical_handle_position; if estimated_horizontal_handle_position > 0 then |