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.)

1 files changed, 19 insertions, 15 deletions

diff --git a/ide/session.ml b/ide/session.ml
index a9c106a765..38fdd0ef2a 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -502,19 +502,25 @@ let build_layout (sn:session) =
       ~callback:(fun () -> if sn.buffer#modified
         then img#set_stock `SAVE
         else img#set_stock `YES) in
-  let _ =
-    eval_paned#misc#connect#size_allocate
-      ~callback:
-      (let b = ref true in
-       fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
-       if !b then begin
-           eval_paned#set_position
-             (paned_width / 2);
-           state_paned#set_position
-             (paned_height / 2);
-           b := false
-	 end)
-  in
+  (* There was an issue in the previous implementation for setting the
+     position of the handle. It was using the size_allocate event but
+     there is an issue with size_allocate. G. Melquiond analyzed that
+     at starting time, the size_allocate event is only issued in
+     Layout phase of the gtk loop so that it is actually processed
+     only in the next iteration of the event-update-layout-paint loop,
+     after the user does something and trigger an effective new event
+     (see #10578). So we preventively enforce an estimated position
+     for the handles to be used in the very first initializing
+     iteration of the loop *)
+  let () =
+    (* 14 is the estimated size for vertical borders *)
+    let estimated_vertical_handle_position = (window_width#get - 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
+    if estimated_vertical_handle_position > 0 then
+      eval_paned#set_position estimated_vertical_handle_position;
+    if estimated_horizontal_handle_position > 0 then
+      state_paned#set_position estimated_horizontal_handle_position in
   session_box#pack sn.finder#coerce;
   session_box#pack sn.segment#coerce;
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
@@ -538,8 +544,6 @@ let build_layout (sn:session) =
     else (label#set_text (red txt);label#set_use_markup true));
   session_tab#pack sn.tab_label#coerce;
   img#set_stock `YES;
-  eval_paned#set_position 1;
-  state_paned#set_position 1;
   let control =
     object
       method detach () = proof_detachable#detach ()