aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Detachable.ml
blob: 9eb1b32320eb97c1333bd653a69ddb0cb744946c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
(************************************************************************)
(*  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

    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))