]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/glGtk.ml
* click signal changed: now the element argument is optional
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / glGtk.ml
1 (* $Id$ *)
2
3 open Gaux
4 open Gtk
5
6 type visual_options = [
7   | `USE_GL
8   | `BUFFER_SIZE of int
9   | `LEVEL of int
10   | `RGBA
11   | `DOUBLEBUFFER
12   | `STEREO
13   | `AUX_BUFFERS of int
14   | `RED_SIZE of int
15   | `GREEN_SIZE of int
16   | `BLUE_SIZE of int
17   | `ALPHA_SIZE of int
18   | `DEPTH_SIZE of int
19   | `STENCIL_SIZE of int
20   | `ACCUM_GREEN_SIZE of int
21   | `ACCUM_ALPHA_SIZE of int
22 ]
23
24 type gl_area = [`widget|`drawing|`glarea]
25
26 module Raw = struct
27   external create :
28     visual_options list -> share:[>`glarea] optobj -> gl_area obj
29     = "ml_gtk_gl_area_new"
30
31   external swap_buffers : [>`glarea] obj -> unit
32     = "ml_gtk_gl_area_swapbuffers"
33
34   external make_current : [>`glarea] obj -> bool
35     = "ml_gtk_gl_area_make_current"
36 end
37
38 class area_signals obj =
39 object (connect)
40   inherit GObj.widget_signals obj
41   method display ~callback =
42     (new GObj.event_signals ~after obj)#expose ~callback:
43       begin fun ev ->
44         if GdkEvent.Expose.count ev = 0 then
45           if Raw.make_current obj then callback ()
46           else prerr_endline "GlGtk-WARNING **: could not make current";
47         true
48       end
49   method reshape ~callback =
50     (new GObj.event_signals ~after obj)#configure ~callback:
51       begin fun ev ->
52         if Raw.make_current obj then begin
53           callback ~width:(GdkEvent.Configure.width ev)
54             ~height:(GdkEvent.Configure.height ev)
55         end
56         else prerr_endline "GlGtk-WARNING **: could not make current";
57         true
58       end
59   method realize ~callback =
60     let connect = new GObj.misc_signals ~after (GtkBase.Widget.coerce obj) in
61     connect#realize ~callback:
62       begin fun ev ->
63         if Raw.make_current obj then callback ()
64         else prerr_endline "GlGtk-WARNING **: could not make current"
65       end
66 end
67
68 class area obj = object (self)
69   inherit GObj.widget (obj : gl_area obj)
70   method as_area = obj
71   method event = new GObj.event_ops obj
72   method connect = new area_signals obj
73   method set_size = GtkMisc.DrawingArea.size obj
74   method swap_buffers () = Raw.swap_buffers obj
75   method make_current () =
76     if not (Raw.make_current obj) then
77       raise (Gl.GLerror "make_current")
78 end
79
80 let area options ?share ?(width=0) ?(height=0) ?packing ?show () =
81   let share =
82     match share with Some (x : area) -> Some x#as_area | None -> None in
83   let w = Raw.create options ~share:(Gpointer.optboxed share) in
84   if width <> 0 || height <> 0 then GtkMisc.DrawingArea.size w ~width ~height;
85   GtkBase.Widget.add_events w [`EXPOSURE];
86   GObj.pack_return (new area w) ~packing ~show