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_Detachable.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_Detachable.ml')
-rw-r--r-- | ide/wg_Detachable.ml | 83 |
1 files changed, 83 insertions, 0 deletions
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml new file mode 100644 index 000000000..787b9aec9 --- /dev/null +++ b/ide/wg_Detachable.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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)) + |