diff options
| author | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-13 15:20:06 +0100 |
| commit | dde10a9b2512ffc7e941c79bbc442c5b4b1f45f9 (patch) | |
| tree | c7e4cbb5b690aaea3a9dedfd516e252fea2ea435 /ide/session.ml | |
| parent | c45f079c52524da687dfcc9e5f5511d6e86bc537 (diff) | |
| parent | 882e37cfa843ff7444525550e7ac3fe44b1fcecb (diff) | |
Merge PR #11070: Do not rely on the user settings but on the actual window size. (Fixes #10956)
Reviewed-by: ppedrot
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 |