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 | |
| 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
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | ide/session.ml | 6 | ||||
| -rw-r--r-- | ide/session.mli | 2 |
3 files changed, 8 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 70fa61b208..14cd87e7b5 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -966,6 +966,8 @@ let build_ui () = with _ -> () in let _ = w#event#connect#delete ~callback:(fun _ -> File.quit ~parent:w (); true) in + let _ = w#misc#connect#size_allocate + ~callback:(fun rect -> window_size := (rect.Gtk.width, rect.Gtk.height)) in let _ = set_drag w#drag in let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in 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 diff --git a/ide/session.mli b/ide/session.mli index f5d8d7c991..63ac1e6dc0 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -51,3 +51,5 @@ val kill : session -> unit val build_layout : session -> GObj.widget option * GObj.widget option * GObj.widget + +val window_size : (int * int) ref |