diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:14 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:14 +0000 |
commit | ad4343b8daf31569fe46c53032ce5fc409076672 (patch) | |
tree | 7672c75cd00842f9170aac78ffacd47bd24ad09c /ide/wg_Command.ml | |
parent | 8a4315ed0852b4a7559da977d7e2aa3fe939dd79 (diff) |
wg_Detachable: move out of wg_Command
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r-- | ide/wg_Command.ml | 78 |
1 files changed, 2 insertions, 76 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 6c0d1c3ad..99caa1c33 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -6,85 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -class type detachable_signals = - object - inherit GContainer.container_signals - method attached : callback:(GObj.widget -> unit) -> unit - method detached : callback:(GObj.widget -> unit) -> unit - end - -class detachable (obj : ([> Gtk.box] as 'a) Gobject.obj) = - - object(self) - inherit GPack.box_skel (obj :> Gtk.box Gobject.obj) as super - - val but = GButton.button () - val win = GWindow.window () - val frame = GBin.frame ~shadow_type:`NONE () - val mutable detached = false - val mutable detached_cb = (fun _ -> ()) - val mutable attached_cb = (fun _ -> ()) - - method child = frame#child - method add = frame#add - method pack ?from ?expand ?fill ?padding w = - if frame#all_children = [] then self#add w - else raise (Invalid_argument "detachable#pack") - - method title = win#title - method set_title = win#set_title - - method connect : detachable_signals = object - inherit GContainer.container_signals_impl obj - method attached ~callback = attached_cb <- callback - method detached ~callback = detached_cb <- callback - end - - method show = - if detached then win#present () - else self#misc#show (); - - method hide = - if detached then win#misc#hide () - else self#misc#hide () - - method visible = win#misc#visible || self#misc#visible - - initializer - self#set_homogeneous false; - super#pack ~expand:false but#coerce; - super#pack ~expand:true ~fill:true frame#coerce; - win#misc#hide (); - but#add (GMisc.label - ~markup:"<span size='x-small'>D\nE\nT\nA\nC\nH</span>" ())#coerce; - ignore(win#event#connect#delete ~callback:(fun _ -> - win#misc#hide (); - frame#misc#reparent self#coerce; - detached <- false; - attached_cb self#child; - true)); - ignore(but#connect#clicked ~callback:(fun _ -> - frame#misc#reparent win#coerce; - self#misc#hide (); - win#present (); - detached <- true; - detached_cb self#child; - )) - - end - -let detachable ?title = - GtkPack.Box.make_params [] ~cont:( - GContainer.pack_container - ~create:(fun p -> - let d = new detachable (GtkPack.Box.create `HORIZONTAL p) in - Option.iter d#set_title title; - d)) - open Preferences class command_window name coqtop = - let frame = detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in + let frame = Wg_Detachable.detachable + ~title:(Printf.sprintf "Query pane (%s)" name) () in let _ = frame#hide in let _ = GtkData.AccelGroup.create () in let notebook = |