]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gdk.mli
* implemented a more efficient selection to avoid flickering
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / gdk.mli
1 (* $Id$ *)
2
3 type colormap
4 type visual
5 type region
6 type gc
7 type 'a drawable
8 type window = [`window] drawable
9 type pixmap = [`pixmap] drawable
10 type bitmap = [`bitmap] drawable
11 type font
12 type image
13 type atom = int
14 type keysym = int
15 type 'a event
16 type drag_context
17 type cursor
18 type xid = int32
19
20 exception Error of string
21
22 module Tags : sig
23   type event_type =
24     [ `NOTHING|`DELETE|`DESTROY|`EXPOSE|`MOTION_NOTIFY|`BUTTON_PRESS
25      |`TWO_BUTTON_PRESS|`THREE_BUTTON_PRESS
26      |`BUTTON_RELEASE|`KEY_PRESS
27      |`KEY_RELEASE|`ENTER_NOTIFY|`LEAVE_NOTIFY|`FOCUS_CHANGE
28      |`CONFIGURE|`MAP|`UNMAP|`PROPERTY_NOTIFY|`SELECTION_CLEAR
29      |`SELECTION_REQUEST|`SELECTION_NOTIFY|`PROXIMITY_IN
30      |`PROXIMITY_OUT|`DRAG_ENTER|`DRAG_LEAVE|`DRAG_MOTION|`DRAG_STATUS
31      |`DROP_START|`DROP_FINISHED|`CLIENT_EVENT|`VISIBILITY_NOTIFY
32      |`NO_EXPOSE ]
33   type event_mask =
34     [ `EXPOSURE
35      |`POINTER_MOTION|`POINTER_MOTION_HINT
36      |`BUTTON_MOTION|`BUTTON1_MOTION|`BUTTON2_MOTION|`BUTTON3_MOTION
37      |`BUTTON_PRESS|`BUTTON_RELEASE
38      |`KEY_PRESS|`KEY_RELEASE
39      |`ENTER_NOTIFY|`LEAVE_NOTIFY|`FOCUS_CHANGE
40      |`STRUCTURE|`PROPERTY_CHANGE|`VISIBILITY_NOTIFY
41      |`PROXIMITY_IN|`PROXIMITY_OUT|`SUBSTRUCTURE
42      |`ALL_EVENTS ]
43   type extension_events = [ `NONE|`ALL|`CURSOR ]
44   type visibility_state = [ `UNOBSCURED|`PARTIAL|`FULLY_OBSCURED ]
45   type input_source = [ `MOUSE|`PEN|`ERASER|`CURSOR ]
46   type notify_type =
47     [ `ANCESTOR|`VIRTUAL|`INFERIOR|`NONLINEAR|`NONLINEAR_VIRTUAL|`UNKNOWN ] 
48   type crossing_mode = [ `NORMAL|`GRAB|`UNGRAB ]
49   type modifier =
50     [ `SHIFT|`LOCK|`CONTROL|`MOD1|`MOD2|`MOD3|`MOD4|`MOD5|`BUTTON1
51      |`BUTTON2|`BUTTON3|`BUTTON4|`BUTTON5 ]
52   type drag_action = [ `DEFAULT|`COPY|`MOVE|`LINK|`PRIVATE|`ASK ]
53 end
54
55 module Convert :
56   sig
57     val modifier : int -> Tags.modifier list
58   end
59
60 module Screen :
61   sig
62     external width : unit -> int = "ml_gdk_screen_width"
63     external height : unit -> int = "ml_gdk_screen_height"
64   end
65
66 module Visual :
67   sig
68     type visual_type =
69       [ `STATIC_GRAY|`GRAYSCALE|`STATIC_COLOR
70        |`PSEUDO_COLOR|`TRUE_COLOR|`DIRECT_COLOR ]
71     external get_best : ?depth:int -> ?kind:visual_type -> unit -> visual
72         = "ml_gdk_visual_get_best"
73     external get_type : visual -> visual_type = "ml_GdkVisual_type"
74     external depth : visual -> int = "ml_GdkVisual_depth"
75     external red_mask : visual -> int = "ml_GdkVisual_red_mask"
76     external red_shift : visual -> int = "ml_GdkVisual_red_shift"
77     external red_prec : visual -> int = "ml_GdkVisual_red_prec"
78     external green_mask : visual -> int = "ml_GdkVisual_green_mask"
79     external green_shift : visual -> int = "ml_GdkVisual_green_shift"
80     external green_prec : visual -> int = "ml_GdkVisual_green_prec"
81     external blue_mask : visual -> int = "ml_GdkVisual_blue_mask"
82     external blue_shift : visual -> int = "ml_GdkVisual_blue_shift"
83     external blue_prec : visual -> int = "ml_GdkVisual_blue_prec"
84   end
85
86 module Image :
87   sig
88     type image_type = [ `FASTEST|`NORMAL|`SHARED ]
89     external create_bitmap :
90       visual:visual -> data:string -> width:int -> height:int -> image
91       = "ml_gdk_image_new_bitmap"
92     external create :
93       kind:image_type ->
94       visual:visual -> width:int -> height:int -> image = "ml_gdk_image_new"
95     external get :
96       'a drawable -> x:int -> y:int -> width:int -> height:int -> image
97       = "ml_gdk_image_get"
98     external put_pixel : image -> x:int -> y:int -> pixel:int -> unit
99       = "ml_gdk_image_put_pixel"
100     external get_pixel : image -> x:int -> y:int -> int
101       = "ml_gdk_image_get_pixel"
102     external destroy : image -> unit = "ml_gdk_image_destroy"
103   end
104
105 module Color :
106   sig
107     external get_system_colormap : unit -> colormap
108         = "ml_gdk_colormap_get_system"
109     val get_colormap : ?privat:bool -> visual -> colormap
110
111     type t
112     type spec = [
113       | `BLACK
114       | `NAME of string
115       | `RGB of int * int * int
116       | `WHITE
117     ]
118     val alloc : colormap:colormap -> spec -> t
119     external red : t -> int = "ml_GdkColor_red"
120     external blue : t -> int = "ml_GdkColor_blue"
121     external green : t -> int = "ml_GdkColor_green"
122     external pixel : t -> int = "ml_GdkColor_pixel"
123   end
124
125 module Rectangle :
126   sig
127     type t
128     external create : x:int -> y:int -> width:int -> height:int -> t
129       = "ml_GdkRectangle"
130     external x : t -> int = "ml_GdkRectangle_x"
131     external y : t -> int = "ml_GdkRectangle_y"
132     external width : t -> int = "ml_GdkRectangle_width"
133     external height : t -> int = "ml_GdkRectangle_height"
134   end
135
136 module Window :
137   sig
138     type background_pixmap = [ `NONE|`PARENT_RELATIVE|`PIXMAP of pixmap ]
139     external visual_depth : visual -> int = "ml_gdk_visual_get_depth"
140     external get_visual : window -> visual = "ml_gdk_window_get_visual"
141     external get_parent : window -> window = "ml_gdk_window_get_parent"
142     external get_size : window -> int * int = "ml_gdk_window_get_size"
143     external get_position : window -> int * int
144       = "ml_gdk_window_get_position"
145     external root_parent : unit -> window = "ml_GDK_ROOT_PARENT"
146     external clear : window -> unit = "ml_gdk_window_clear"
147     external get_xwindow : window -> xid = "ml_GDK_WINDOW_XWINDOW"
148     val set_back_pixmap : window -> background_pixmap -> unit
149   end
150
151 module PointArray :
152   sig
153     type t = { len: int }
154     external create : len:int -> t = "ml_point_array_new"
155     val set : t -> pos:int -> x:int -> y:int -> unit
156   end
157
158 module Region :
159   sig
160     type gdkFillRule = [ `EVEN_ODD_RULE|`WINDING_RULE ]
161     type gdkOverlapType = [ `IN|`OUT|`PART ]
162     external create : unit -> region = "ml_gdk_region_new"
163     external destroy : region -> unit = "ml_gdk_region_destroy"
164     val polygon : (int * int) list -> gdkFillRule -> region 
165     external intersect : region -> region -> region
166       = "ml_gdk_regions_intersect"
167     external union : region -> region -> region 
168       = "ml_gdk_regions_union"
169     external subtract : region -> region -> region 
170       = "ml_gdk_regions_subtract"
171     external xor : region -> region -> region 
172       = "ml_gdk_regions_xor"
173     external union_with_rect : region -> Rectangle.t -> region
174       = "ml_gdk_region_union_with_rect"
175     external offset : region -> x:int -> y:int -> unit = "ml_gdk_region_offset"
176     external shrink : region -> x:int -> y:int -> unit = "ml_gdk_region_shrink"
177     external empty : region -> bool = "ml_gdk_region_empty"
178     external equal : region -> region -> bool = "ml_gdk_region_equal"
179     external point_in : region -> x:int -> y:int -> bool 
180       = "ml_gdk_region_point_in"
181     external rect_in : region -> Rectangle.t -> gdkOverlapType
182       = "ml_gdk_region_rect_in"
183     external get_clipbox : region -> Rectangle.t -> unit
184       = "ml_gdk_region_get_clipbox"
185   end
186
187 module GC :
188   sig
189     type gdkFunction = [ `COPY|`INVERT|`XOR ]
190     type gdkFill = [ `SOLID|`TILED|`STIPPLED|`OPAQUE_STIPPLED ]
191     type gdkSubwindowMode = [ `CLIP_BY_CHILDREN|`INCLUDE_INFERIORS ]
192     type gdkLineStyle = [ `SOLID|`ON_OFF_DASH|`DOUBLE_DASH ]
193     type gdkCapStyle = [ `NOT_LAST|`BUTT|`ROUND|`PROJECTING ]
194     type gdkJoinStyle = [ `MITER|`ROUND|`BEVEL ]
195     external create : 'a drawable -> gc = "ml_gdk_gc_new"
196     external set_foreground : gc -> Color.t -> unit
197       = "ml_gdk_gc_set_foreground"
198     external set_background : gc -> Color.t -> unit
199       = "ml_gdk_gc_set_background"
200     external set_font : gc -> font -> unit = "ml_gdk_gc_set_font"
201     external set_function : gc -> gdkFunction -> unit
202       = "ml_gdk_gc_set_function"
203     external set_fill : gc -> gdkFill -> unit = "ml_gdk_gc_set_fill"
204     external set_tile : gc -> pixmap -> unit = "ml_gdk_gc_set_tile"
205     external set_stipple : gc -> pixmap -> unit = "ml_gdk_gc_set_stipple"
206     external set_ts_origin : gc -> x:int -> y:int -> unit
207       = "ml_gdk_gc_set_ts_origin"
208     external set_clip_origin : gc -> x:int -> y:int -> unit
209       = "ml_gdk_gc_set_clip_origin"
210     external set_clip_mask : gc -> bitmap -> unit = "ml_gdk_gc_set_clip_mask"
211     external set_clip_rectangle : gc -> Rectangle.t -> unit
212       = "ml_gdk_gc_set_clip_rectangle"
213     external set_clip_region : gc -> region -> unit
214         = "ml_gdk_gc_set_clip_region"
215     external set_subwindow : gc -> gdkSubwindowMode -> unit
216       = "ml_gdk_gc_set_subwindow"
217     external set_exposures : gc -> bool -> unit = "ml_gdk_gc_set_exposures"
218     external set_line_attributes :
219       gc ->
220       width:int ->
221       style:gdkLineStyle -> cap:gdkCapStyle -> join:gdkJoinStyle -> unit
222       = "ml_gdk_gc_set_line_attributes"
223     external copy : dst:gc -> gc -> unit = "ml_gdk_gc_copy"
224     type values = {
225         foreground : Color.t;
226         background : Color.t;
227         font : font option;
228         fonction : gdkFunction;
229         fill : gdkFill;
230         tile : pixmap option;
231         stipple : pixmap option;
232         clip_mask : bitmap option;
233         subwindow_mode : gdkSubwindowMode;
234         ts_x_origin : int;
235         ts_y_origin : int;
236         clip_x_origin : int;
237         clip_y_origin : int;
238         graphics_exposures : bool;
239         line_width : int;
240         line_style : gdkLineStyle;
241         cap_style : gdkCapStyle;
242         join_style : gdkJoinStyle;
243       }
244     external get_values : gc -> values = "ml_gdk_gc_get_values"
245   end
246
247 module Pixmap :
248   sig
249     external create :
250       window -> width:int -> height:int -> depth:int -> pixmap
251       = "ml_gdk_pixmap_new"
252     external create_from_data :
253       window ->
254       string ->
255       width:int ->
256       height:int -> depth:int -> fg:Color.t -> bg:Color.t -> pixmap
257       = "ml_gdk_pixmap_create_from_data_bc" "ml_gk_pixmap_create_from_data"
258     external create_from_xpm :
259       window ->
260       ?colormap:colormap ->
261       ?transparent:Color.t -> file:string -> pixmap * bitmap
262       = "ml_gdk_pixmap_colormap_create_from_xpm"
263     external create_from_xpm_d :
264       window ->
265       ?colormap:colormap ->
266       ?transparent:Color.t -> data:string array -> pixmap * bitmap
267       = "ml_gdk_pixmap_colormap_create_from_xpm_d"
268   end
269
270 module Bitmap :
271   sig
272     val create : window -> width:int -> height:int -> bitmap
273     external create_from_data :
274       window -> string -> width:int -> height:int -> bitmap
275       = "ml_gdk_bitmap_create_from_data"
276   end
277
278 module Font :
279   sig
280     external load : string -> font = "ml_gdk_font_load"
281     external load_fontset : string -> font = "ml_gdk_fontset_load"
282     external string_width : font -> string -> int = "ml_gdk_string_width"
283     external char_width : font -> char -> int = "ml_gdk_char_width"
284     external string_height : font -> string -> int = "ml_gdk_string_height"
285     external char_height : font -> char -> int = "ml_gdk_char_height"
286     external string_measure : font -> string -> int = "ml_gdk_string_measure"
287     external char_measure : font -> char -> int = "ml_gdk_char_measure"
288     external get_type : font -> [`FONT | `FONTSET] = "ml_GdkFont_type"
289     external ascent : font -> int = "ml_GdkFont_ascent"
290     external descent : font -> int = "ml_GdkFont_descent"
291   end
292
293 module Draw :
294   sig
295     external point : 'a drawable -> gc -> x:int -> y:int -> unit
296       = "ml_gdk_draw_point"
297     external line :
298       'a drawable -> gc -> x:int -> y:int -> x:int -> y:int -> unit
299       = "ml_gdk_draw_line_bc" "ml_gdk_draw_line"
300     val rectangle :
301       'a drawable -> gc ->
302       x:int -> y:int -> width:int -> height:int -> ?filled:bool -> unit -> unit
303     val arc :
304       'a drawable -> gc ->
305       x:int -> y:int -> width:int -> height:int ->
306       ?filled:bool -> ?start:float -> ?angle:float -> unit -> unit
307     val polygon :
308       'a drawable -> gc -> ?filled:bool ->(int * int) list -> unit
309     external string :
310       'a drawable ->
311       font:font -> gc -> x:int -> y:int -> string:string -> unit
312       = "ml_gdk_draw_string_bc" "ml_gdk_draw_string"
313     external image :
314       'a drawable ->
315       gc ->
316       image:image ->
317       xsrc:int ->
318       ysrc:int -> xdest:int -> ydest:int -> width:int -> height:int -> unit
319       = "ml_gdk_draw_image_bc" "ml_gdk_draw_image"
320   end
321
322 module Rgb :
323   sig
324     external init : unit -> unit = "ml_gdk_rgb_init"
325     external get_visual : unit -> visual = "ml_gdk_rgb_get_visual"
326     external get_cmap : unit -> colormap = "ml_gdk_rgb_get_cmap"
327   end
328
329 module DnD :
330   sig
331     external drag_status :
332       drag_context -> Tags.drag_action list -> time:int -> unit
333       = "ml_gdk_drag_status"
334     external drag_context_suggested_action : drag_context -> Tags.drag_action
335       = "ml_GdkDragContext_suggested_action"
336     external drag_context_targets : drag_context -> atom list
337       = "ml_GdkDragContext_targets"
338   end
339
340 module Truecolor :
341   sig
342     val color_creator : visual -> (red: int -> green: int -> blue: int -> int)
343         (* [color_creator visual] creates a function to calculate 
344            the pixel color id for given red, green and blue component 
345            value ([0..65535]) at the client side. [visual] must have 
346            `TRUE_COLOR or `DIRECT_COLOR type. This function improves
347            the speed of the color query of true color visual greatly. *)
348         (* WARN: this approach is not theoretically correct for true color
349            visual, because we need gamma correction. *)
350
351     val color_parser : visual -> int -> int * int * int
352   end
353
354 module X :
355   (* X related functions *)
356   sig
357     val flush : unit -> unit (* also in GtkMain *)
358     val beep : unit -> unit
359   end
360
361 module Cursor : sig
362   type cursor_type = [
363     | `X_CURSOR
364     | `ARROW
365     | `BASED_ARROW_DOWN
366     | `BASED_ARROW_UP
367     | `BOAT
368     | `BOGOSITY
369     | `BOTTOM_LEFT_CORNER
370     | `BOTTOM_RIGHT_CORNER
371     | `BOTTOM_SIDE
372     | `BOTTOM_TEE
373     | `BOX_SPIRAL
374     | `CENTER_PTR
375     | `CIRCLE
376     | `CLOCK
377     | `COFFEE_MUG
378     | `CROSS
379     | `CROSS_REVERSE
380     | `CROSSHAIR
381     | `DIAMOND_CROSS
382     | `DOT
383     | `DOTBOX
384     | `DOUBLE_ARROW
385     | `DRAFT_LARGE
386     | `DRAFT_SMALL
387     | `DRAPED_BOX
388     | `EXCHANGE
389     | `FLEUR
390     | `GOBBLER
391     | `GUMBY
392     | `HAND1
393     | `HAND2
394     | `HEART
395     | `ICON
396     | `IRON_CROSS
397     | `LEFT_PTR
398     | `LEFT_SIDE
399     | `LEFT_TEE
400     | `LEFTBUTTON
401     | `LL_ANGLE
402     | `LR_ANGLE
403     | `MAN
404     | `MIDDLEBUTTON
405     | `MOUSE
406     | `PENCIL
407     | `PIRATE
408     | `PLUS
409     | `QUESTION_ARROW
410     | `RIGHT_PTR
411     | `RIGHT_SIDE
412     | `RIGHT_TEE
413     | `RIGHTBUTTON
414     | `RTL_LOGO
415     | `SAILBOAT
416     | `SB_DOWN_ARROW
417     | `SB_H_DOUBLE_ARROW
418     | `SB_LEFT_ARROW
419     | `SB_RIGHT_ARROW
420     | `SB_UP_ARROW
421     | `SB_V_DOUBLE_ARROW
422     | `SHUTTLE
423     | `SIZING
424     | `SPIDER
425     | `SPRAYCAN
426     | `STAR
427     | `TARGET
428     | `TCROSS
429     | `TOP_LEFT_ARROW
430     | `TOP_LEFT_CORNER
431     | `TOP_RIGHT_CORNER
432     | `TOP_SIDE
433     | `TOP_TEE
434     | `TREK
435     | `UL_ANGLE
436     | `UMBRELLA
437     | `UR_ANGLE
438     | `WATCH
439     | `XTERM
440   ]
441   external create : cursor_type -> cursor = "ml_gdk_cursor_new"
442   external create_from_pixmap :
443     pixmap -> mask:bitmap ->
444     fg:Color.t -> bg:Color.t -> x:int -> y:int -> cursor
445     = "ml_gdk_cursor_new_from_pixmap_bc" "ml_gdk_cursor_new_from_pixmap"
446   external destroy : cursor -> unit = "ml_gdk_cursor_destroy"
447 end