]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gdkEvent.ml
- DoubleTypeInference.does_not_occur exposed
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / gdkEvent.ml
1 (* $Id$ *)
2
3 open Gaux
4 open Gdk
5 open Tags
6
7 external coerce : 'a event -> event_type event = "%identity"
8 external unsafe_copy : Gpointer.boxed -> #event_type event
9     = "ml_gdk_event_copy"
10 external copy : (#event_type as 'a) event -> 'a event
11     = "ml_gdk_event_copy"
12 external get_type : 'a event -> 'a = "ml_GdkEventAny_type"
13 external get_window : 'a event -> window = "ml_GdkEventAny_window"
14 external get_send_event : 'a event -> bool = "ml_GdkEventAny_send_event"
15
16 external create : (#event_type as 'a) -> 'a event
17     = "ml_gdk_event_new"
18 external set_window : 'a event -> window -> unit
19     = "ml_gdk_event_set_window"
20
21 module Expose = struct
22   type t = [ `EXPOSE ] event
23   let cast (ev : event_type event) : t =
24     match get_type ev with `EXPOSE -> Obj.magic ev
25     | _ -> invalid_arg "GdkEvent.Expose.cast"
26   external area : t -> Rectangle.t = "ml_GdkEventExpose_area"
27   external count : t -> int = "ml_GdkEventExpose_count"
28 end
29
30 module Visibility = struct
31   type t = [ `VISIBILITY_NOTIFY ] event
32   let cast (ev :  event_type event) : t =
33     match get_type ev with `VISIBILITY_NOTIFY -> Obj.magic ev
34     | _ -> invalid_arg "GdkEvent.Visibility.cast"
35   external visibility : t -> visibility_state
36       = "ml_GdkEventVisibility_state"
37 end
38
39 module Motion = struct
40   type t = [ `MOTION_NOTIFY ] event
41   let cast (ev : event_type event) : t =
42     match get_type ev with `MOTION_NOTIFY -> Obj.magic ev
43     | _ -> invalid_arg "GdkEvent.Motion.cast"
44   external time : t -> int = "ml_GdkEventMotion_time"
45   external x : t -> float = "ml_GdkEventMotion_x"
46   external y : t -> float = "ml_GdkEventMotion_y"
47   external pressure : t -> float = "ml_GdkEventMotion_pressure"
48   external xtilt : t -> float = "ml_GdkEventMotion_xtilt"
49   external ytilt : t -> float = "ml_GdkEventMotion_ytilt"
50   external state : t -> int = "ml_GdkEventMotion_state"
51   external is_hint : t -> bool = "ml_GdkEventMotion_is_hint"
52   external source : t -> input_source = "ml_GdkEventMotion_source"
53   external deviceid : t -> int = "ml_GdkEventMotion_deviceid"
54   external x_root : t -> float = "ml_GdkEventMotion_x_root"
55   external y_root : t -> float = "ml_GdkEventMotion_y_root"
56 end
57
58 module Button = struct
59   type types =
60       [ `BUTTON_PRESS|`TWO_BUTTON_PRESS|`THREE_BUTTON_PRESS|`BUTTON_RELEASE ]
61   type t = types event
62   let cast (ev : event_type event) : t =
63     match get_type ev with
64       `BUTTON_PRESS|`TWO_BUTTON_PRESS|`THREE_BUTTON_PRESS|`BUTTON_RELEASE
65       -> Obj.magic ev
66     | _ -> invalid_arg "GdkEvent.Button.cast"
67   external time : t -> int = "ml_GdkEventButton_time"
68   external x : t -> float = "ml_GdkEventButton_x"
69   external y : t -> float = "ml_GdkEventButton_y"
70   external pressure : t -> float = "ml_GdkEventButton_pressure"
71   external xtilt : t -> float = "ml_GdkEventButton_xtilt"
72   external ytilt : t -> float = "ml_GdkEventButton_ytilt"
73   external state : t -> int = "ml_GdkEventButton_state"
74   external button : t -> int = "ml_GdkEventButton_button"
75   external source : t -> input_source = "ml_GdkEventButton_source"
76   external deviceid : t -> int = "ml_GdkEventButton_deviceid"
77   external x_root : t -> float = "ml_GdkEventButton_x_root"
78   external y_root : t -> float = "ml_GdkEventButton_y_root"
79   external set_type : t -> #types -> unit
80       = "ml_gdk_event_set_type"
81   external set_button : t -> int -> unit
82       = "ml_gdk_event_button_set_button"
83 end
84
85 module Key = struct
86   type t = [ `KEY_PRESS|`KEY_RELEASE ] event
87   let cast (ev : event_type event) : t =
88     match get_type ev with
89       `KEY_PRESS|`KEY_RELEASE -> Obj.magic ev
90     | _ -> invalid_arg "GdkEvent.Key.cast"
91   external time : t -> int = "ml_GdkEventKey_time"
92   external state : t -> int = "ml_GdkEventKey_state"
93   external keyval : t -> keysym = "ml_GdkEventKey_keyval"
94   external string : t -> string = "ml_GdkEventKey_string"
95   let state ev = Convert.modifier (state ev)
96 end
97
98 module Crossing = struct
99   type t = [ `ENTER_NOTIFY|`LEAVE_NOTIFY ] event
100   let cast (ev : event_type event) : t =
101     match get_type ev with
102       `ENTER_NOTIFY|`LEAVE_NOTIFY -> Obj.magic ev
103     | _ -> invalid_arg "GdkEvent.Crossing.cast"
104   external subwindow : t -> window = "ml_GdkEventCrossing_subwindow"
105   external detail : t -> notify_type = "ml_GdkEventCrossing_detail"
106 end
107
108 module Focus = struct
109   type t = [ `FOCUS_CHANGE ] event
110   let cast (ev : event_type event) : t =
111     match get_type ev with `FOCUS_CHANGE -> Obj.magic ev
112     | _ -> invalid_arg "GdkEvent.Focus.cast"
113   external focus_in : t -> bool = "ml_GdkEventFocus_in"
114 end
115
116 module Configure = struct
117   type t = [ `CONFIGURE ] event
118   let cast (ev : event_type event) : t =
119     match get_type ev with `CONFIGURE -> Obj.magic ev
120     |   _ -> invalid_arg "GdkEvent.Configure.cast"
121   external x : t -> int = "ml_GdkEventConfigure_x"
122   external y : t -> int = "ml_GdkEventConfigure_y"
123   external width : t -> int = "ml_GdkEventConfigure_width"
124   external height : t -> int = "ml_GdkEventConfigure_height"
125 end
126
127 module Property = struct
128   type t = [ `PROPERTY_NOTIFY ] event
129   let cast (ev : event_type event) : t =
130     match get_type ev with `PROPERTY_NOTIFY -> Obj.magic ev
131     | _ -> invalid_arg "GdkEvent.Property.cast"
132   external atom : t -> atom = "ml_GdkEventProperty_atom"
133   external time : t -> int = "ml_GdkEventProperty_time"
134   external state : t -> int = "ml_GdkEventProperty_state"
135 end
136
137 module Selection = struct
138   type t = [ `SELECTION_CLEAR|`SELECTION_REQUEST|`SELECTION_NOTIFY ] event
139   let cast (ev : event_type event) : t =
140     match get_type ev with
141       `SELECTION_CLEAR|`SELECTION_REQUEST|`SELECTION_NOTIFY -> Obj.magic ev
142     | _ -> invalid_arg "GdkEvent.Selection.cast"
143   external selection : t -> atom = "ml_GdkEventSelection_selection"
144   external target : t -> atom = "ml_GdkEventSelection_target"
145   external property : t -> atom = "ml_GdkEventSelection_property"
146   external requestor : t -> int = "ml_GdkEventSelection_requestor"
147   external time : t -> int = "ml_GdkEventSelection_time"
148 end
149
150 module Proximity = struct
151   type t = [ `PROXIMITY_IN|`PROXIMITY_OUT ] event
152   let cast (ev : event_type event) : t =
153     match get_type ev with
154       `PROXIMITY_IN|`PROXIMITY_OUT -> Obj.magic ev
155     | _ -> invalid_arg "GdkEvent.Proximity.cast"
156   external time : t -> int = "ml_GdkEventProximity_time"
157   external source : t -> input_source = "ml_GdkEventProximity_source"
158   external deviceid : t -> int = "ml_GdkEventProximity_deviceid"
159 end