Now windows resize well (at least some of them)

[helm.git] / helm / interface / mmlinterface.ml

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 2dfc5e4f9f8cadd2e60476b0b3ba5a47409f1b12..784c9f4b127e47a21089047296af4dc079675dfa 100755 (executable)
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -230,7 +230,7 @@ let jump rendering_window node =
 
 let choose_selection rendering_window node =
  let module M = Minidom in
- let rec aux ~first_time node =
+ let rec aux node =
   match M.node_get_attribute node (M.mDOMString_of_string "xref") with
      None ->
       let parent =
@@ -238,14 +238,12 @@ let choose_selection rendering_window node =
           None -> assert false
         | Some parent -> parent
       in
-       aux ~first_time:false parent
-   | Some s ->
-      if not first_time then
-       !(rendering_window#output)#set_selection (Some node)
+       aux parent
+   | Some s -> !(rendering_window#output)#set_selection (Some node)
  in
   match node with
-     None      -> () (* No element selected *)
-   | Some node -> aux ~first_time:true node
+     None      -> !(rendering_window#output)#set_selection None
+   | Some node -> aux node
 ;;
 
 
@@ -590,7 +588,7 @@ class rendering_window annotation_window output (label : GMisc.label) =
   GPack.vbox ~packing:window#add () in
  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let _ = scrolled_window0#add !output#coerce in
@@ -656,7 +654,7 @@ class theory_rendering_window rendering_window =
   GMisc.label ~text:"???"
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let output =