diff options
| -rw-r--r-- | ide/command_windows.ml | 36 | ||||
| -rw-r--r-- | ide/command_windows.mli | 4 | ||||
| -rw-r--r-- | ide/coqide.ml | 20 |
3 files changed, 33 insertions, 27 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index b933b7ce2c..c9eb8ad2d0 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -9,17 +9,19 @@ (* $Id$ *) class command_window () = - let window = GWindow.window +(* let window = GWindow.window ~allow_grow:true ~allow_shrink:true ~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 vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in let toolbar = GButton.toolbar ~orientation:`HORIZONTAL - ~style:`ICONS + ~style:`BOTH ~tooltips:true ~packing:(vbox#pack ~expand:false @@ -35,10 +37,10 @@ class command_window () = in let _ = toolbar#insert_button - ~tooltip:"Hide Window" - ~text:"Hide Window" + ~tooltip:"Hide Commands Pane" + ~text:"Hide Pane" ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE) - ~callback:window#misc#hide + ~callback:frame#misc#hide () in let new_page_menu = @@ -46,28 +48,24 @@ class command_window () = ~tooltip:"New Page" ~text:"New Page" ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW) -(* - ~callback:window#misc#hide -*) () in let _ = toolbar#insert_button - ~tooltip:"Kill Page" - ~text:"Kill Page" + ~tooltip:"Delete Page" + ~text:"Delete Page" ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `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 diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 5b060db24d..4104f086c2 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -12,10 +12,10 @@ class command_window : unit -> object method new_command : ?command:string -> ?term:string -> unit -> unit - method window : GWindow.window + method frame : GBin.frame end -val main : unit -> unit + val main : unit -> unit val command_window : unit -> command_window diff --git a/ide/coqide.ml b/ide/coqide.ml index 9bd3f86795..a7618c97b4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3073,17 +3073,20 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"<CoqIde MenuBar>/Windows" ~accel_group in let _ = - configuration_factory#add_item - "Show _Query Window" + configuration_factory#add_check_item + "Show/Hide _Query Pane" (* ~key:GdkKeysyms._F12 *) - ~callback:(Command_windows.command_window ())#window#present + ~callback:(fun b -> if b then + (Command_windows.command_window ())#frame#misc#show () + else + (Command_windows.command_window ())#frame#misc#hide ()) in let _ = - configuration_factory#add_item + configuration_factory#add_check_item "Show/Hide _Toolbar" - ~callback:(fun () -> + ~callback:(fun _ -> !current.show_toolbar <- not !current.show_toolbar; !show_toolbar !current.show_toolbar) in @@ -3170,7 +3173,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* End of menu *) (* The vertical Separator between Scripts and Goals *) - let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:vbox#add () in + let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in + let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true ~packing:fr_notebook#add @@ -3188,6 +3192,10 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(fr_b#add) () in + let command_object = Command_windows.command_window() in + let queries_frame = command_object#frame in + queries_pane#pack2 ~shrink:true ~resize:true (queries_frame#coerce); + let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () in |