diff options
Diffstat (limited to 'ide/command_windows.ml')
| -rw-r--r-- | ide/command_windows.ml | 50 |
1 files changed, 24 insertions, 26 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 937098b7..b84b0943 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,28 +6,30 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *) +(* $Id: command_windows.ml 11042 2008-06-03 12:45:38Z jnarboux $ *) class command_window () = - let window = GWindow.window +(* let window = GWindow.window ~allow_grow:true ~allow_shrink:true - ~width:320 ~height:200 + ~width:500 ~height:250 ~position:`CENTER ~title:"CoqIde queries" ~show:false () - in + in *) + let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in + let _ = frame#misc#hide () in let _ = GtkData.AccelGroup.create () in - let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in + let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in let toolbar = GButton.toolbar - ~orientation:`HORIZONTAL + ~orientation:`VERTICAL ~style:`ICONS ~tooltips:true - ~packing:(vbox#pack + ~packing:(hbox#pack ~expand:false ~fill:false) () in let notebook = GPack.notebook ~scrollable:true - ~packing:(vbox#pack + ~packing:(hbox#pack ~expand:true ~fill:true ) @@ -35,39 +37,35 @@ class command_window () = in let _ = toolbar#insert_button - ~tooltip:"Hide Window" - ~text:"Hide Window" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE) - ~callback:window#misc#hide + ~tooltip:"Hide Commands Pane" + ~text:"Hide Pane" + ~icon:(Ideutils.stock_to_widget `CLOSE) + ~callback:frame#misc#hide () in let new_page_menu = toolbar#insert_button ~tooltip:"New Page" ~text:"New Page" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW) -(* - ~callback:window#misc#hide -*) + ~icon:(Ideutils.stock_to_widget `NEW) () in let _ = toolbar#insert_button - ~tooltip:"Kill Page" - ~text:"Kill Page" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `DELETE) + ~tooltip:"Delete Page" + ~text:"Delete Page" + ~icon:(Ideutils.stock_to_widget `DELETE) ~callback:(fun () -> notebook#remove_page notebook#current_page) () in object(self) - val window = window -(* - val menubar = menubar -*) + val frame = frame + + val new_page_menu = new_page_menu val notebook = notebook - method window = window + method frame = frame method new_command ?command ?term () = let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame @@ -136,11 +134,11 @@ object(self) entry#misc#grab_default (); ignore (entry#connect#activate ~callback); ignore (combo#entry#connect#activate ~callback); - self#window#present () + self#frame#misc#show () initializer ignore (new_page_menu#connect#clicked self#new_command); - ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true)); + (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) end let command_window = ref None |