diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /ide/wg_Detachable.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'ide/wg_Detachable.ml')
-rw-r--r-- | ide/wg_Detachable.ml | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/ide/wg_Detachable.ml b/ide/wg_Detachable.ml new file mode 100644 index 00000000..53c634d7 --- /dev/null +++ b/ide/wg_Detachable.ml @@ -0,0 +1,89 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \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 + + method frame = frame + + method button = but + + method attach () = + win#misc#hide (); + frame#misc#reparent self#coerce; + detached <- false; + attached_cb self#child + + method detach () = + frame#misc#reparent win#coerce; + self#misc#hide (); + win#present (); + detached <- true; + detached_cb self#child + + 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 _ -> self#attach (); true)); + ignore(but#connect#clicked ~callback:(fun _ -> self#detach ())) + + 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)) + |