diff options
| -rw-r--r-- | ide/command_windows.ml | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 5 |
2 files changed, 5 insertions, 3 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index b696704ee..5887492ce 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -69,9 +69,10 @@ object(self) val notebook = notebook method window = window method new_command ?command ?term () = + let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:notebook#append_page + ~packing:appendp () in notebook#goto_page (notebook#page_num frame#coerce); diff --git a/ide/coqide.ml b/ide/coqide.ml index cf18d0ae4..08afda00b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1727,9 +1727,10 @@ let create_input_tab filename = let v_box = GPack.hbox ~homogeneous:false () in let _ = GMisc.image ~packing:v_box#pack () in let _ = GMisc.label ~text:filename ~packing:v_box#pack () in + let appendp x = ignore ((notebook ())#append_page + ~tab_label:v_box#coerce x) in let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:((notebook ())#append_page - ~tab_label:v_box#coerce) () + ~packing:appendp () in let sw1 = GBin.scrolled_window ~vpolicy:`AUTOMATIC |