]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gtk_tags.var
Initial revision
[helm.git] / helm / DEVEL / lablgtk / lablgtk_20000829-0.1.0 / gtk_tags.var
1 (* $Id$ *)
2
3 exception ml_raise_gtk
4
5 type arrow_type = "GTK_ARROW_"
6   [ `UP | `DOWN | `LEFT | `RIGHT ]
7
8 type attach_options = "GTK_"
9   [ `EXPAND | `SHRINK | `FILL ]
10
11 type button_box_style = "GTK_BUTTONBOX_"
12   [ `DEFAULT_STYLE | `SPREAD | `EDGE | `START | `END ]
13
14 type direction_type = "GTK_DIR_"
15   [ `TAB_FORWARD | `TAB_BACKWARD | `UP | `DOWN | `LEFT | `RIGHT ]
16
17 type justification = "GTK_JUSTIFY_"
18   [ `LEFT | `RIGHT | `CENTER | `FILL ]
19
20 type match_type = "GTK_MATCH_"
21   [ `ALL | `ALL_TAIL | `HEAD | `TAIL | `EXACT | `LAST ]
22
23 type metric_type = "GTK_"
24   [ `PIXELS | `INCHES | `CENTIMETERS ]
25
26 type orientation = "GTK_ORIENTATION_"
27   [ `HORIZONTAL | `VERTICAL ]
28
29 type corner_type = "GTK_CORNER_"
30   [ `TOP_LEFT | `BOTTOM_LEFT | `TOP_RIGHT | `BOTTOM_RIGHT ]
31
32 type pack_type = "GTK_PACK_"
33   [ `START | `END ]
34
35 type path_type = "GTK_PATH_"
36   [ `WIDGET | `WIDGET_CLASS | `CLASS ]
37
38 type policy_type = "GTK_POLICY_"
39   [ `ALWAYS | `AUTOMATIC | `NEVER ]
40
41 type position = "GTK_POS_"
42   [ `LEFT | `RIGHT | `TOP | `BOTTOM ]
43
44 type preview_type = "GTK_PREVIEW_"
45   [ `COLOR | `GRAYSCALE ]
46
47 type relief_style = "GTK_RELIEF_"
48   [ `NORMAL | `HALF | `NONE ]
49
50 type resize_mode = "GTK_RESIZE_"
51   [ `PARENT | `QUEUE | `IMMEDIATE ]
52
53 type signal_run_type = "GTK_RUN_"
54   [ `FIRST | `LAST | `BOTH | `NO_RECURSE | `ACTION | `NO_HOOKS ]
55
56 type scroll_type = "GTK_SCROLL_"
57   [ `NONE | `STEP_FORWARD | `STEP_BACKWARD | `PAGE_BACKWARD
58   | `PAGE_FORWARD | `JUMP ]
59
60 type selection_mode = "GTK_SELECTION_"
61   [ `SINGLE | `BROWSE | `MULTIPLE | `EXTENDED ]
62
63 type shadow_type = "GTK_SHADOW_"
64   [ `NONE | `IN | `OUT | `ETCHED_IN | `ETCHED_OUT ]
65
66 type state_type = "GTK_STATE_"
67   [ `NORMAL | `ACTIVE | `PRELIGHT | `SELECTED | `INSENSITIVE ] 
68
69 type submenu_direction = "GTK_DIRECTION_"
70   [ `LEFT | `RIGHT ]
71
72 type submenu_placement = "GTK_"
73   [ `TOP_BOTTOM | `LEFT_RIGHT ]
74
75 type toolbar_style = "GTK_TOOLBAR_"
76   [ `ICONS | `TEXT | `BOTH ]
77
78 type trough_type = "GTK_TROUGH_"
79   [ `NONE | `START | `END | `JUMP ]
80
81 type update_type = "GTK_UPDATE_"
82   [ `CONTINUOUS | `DISCONTINUOUS | `DELAYED ]
83
84 type visibility = "GTK_VISIBILITY_"
85   [ `NONE | `PARTIAL | `FULL ]
86
87 type window_position = "GTK_WIN_POS_"
88   [ `NONE | `CENTER | `MOUSE | `CENTER_ALWAYS ]
89
90 type window_type = "GTK_WINDOW_"
91   [ `TOPLEVEL | `DIALOG | `POPUP ]
92
93 type sort_type = "GTK_SORT_"
94   [ `ASCENDING | `DESCENDING ]
95
96
97 type fundamental_type = "GTK_TYPE_"
98   [ `INVALID | `NONE | `CHAR | `BOOL | `INT | `UINT | `LONG | `ULONG
99   | `FLOAT | `DOUBLE | `STRING | `ENUM | `FLAGS | `BOXED | `FOREIGN
100   | `CALLBACK | `ARGS | `POINTER | `SIGNAL | `C_CALLBACK | `OBJECT ]
101
102 type cell_type = "GTK_CELL_"
103   [ `EMPTY | `TEXT | `PIXMAP | `PIXTEXT | `WIDGET ]
104
105 type toolbar_child = "GTK_TOOLBAR_CHILD_"
106   [ `SPACE | `BUTTON | `TOGGLEBUTTON | `RADIOBUTTON | `WIDGET ]
107
108 type toolbar_space_style = "GTK_TOOLBAR_SPACE_"
109   [ `EMPTY | `LINE ]
110
111 type tree_view_mode = "GTK_TREE_VIEW_"
112   [ `LINE | `ITEM ]
113
114 type spin_type = "GTK_SPIN_"
115   [ `STEP_FORWARD | `STEP_BACKWARD | `PAGE_FORWARD | `PAGE_BACKWARD
116   | `HOME | `END | `USER_DEFINED ]
117
118 type accel_flag = "GTK_ACCEL_"
119   [ `VISIBLE | `SIGNAL_VISIBLE | `LOCKED ]
120
121 type packer_options = "GTK_"
122   [ `PACK_EXPAND | `FILL_X | `FILL_Y ]
123
124 type side_type = "GTK_SIDE_"
125   [ `TOP | `BOTTOM | `LEFT | `RIGHT ]
126
127 type anchor_type = "GTK_ANCHOR_"
128   [ `CENTER | `NORTH | `NW | `NE | `SOUTH | `SW | `SE | `WEST | `EAST ]
129
130 type button_action = "GTK_BUTTON_"
131   [ `SELECTS | `DRAGS | `EXPANDS ]
132
133 type calendar_display_options = "GTK_CALENDAR_"
134   [ `SHOW_HEADING | `SHOW_DAY_NAMES | `NO_MONTH_CHANGE | `SHOW_WEEK_NUMBERS
135   | `WEEK_START_MONDAY ]
136
137 type progress_bar_style = "GTK_PROGRESS_"
138   [ `CONTINUOUS | `DISCRETE ]
139
140 type progress_bar_orientation = "GTK_PROGRESS_"
141   [ `LEFT_TO_RIGHT | `RIGHT_TO_LEFT | `BOTTOM_TO_TOP | `TOP_TO_BOTTOM ]
142
143 type dest_defaults = "GTK_DEST_DEFAULT_"
144   [ `MOTION | `HIGHLIGHT | `DROP | `ALL ]
145
146 type target_flags = "GTK_TARGET_"
147   [ `SAME_APP | `SAME_WIDGET ]
148
149 type font_metric_type = "GTK_FONT_METRIC_"
150   [ `PIXELS | `POINTS ]
151
152 type font_type = "GTK_FONT_"
153   [ `BITMAP | `SCALABLE | `SCALABLE_BITMAP | `ALL ]
154
155 type font_filter_type = "GTK_FONT_FILTER_"
156   [ `BASE | `USER ]
157
158 (*
159 type tree_pos = "GTK_CTREE_POS_"
160   [ `BEFORE | `AS_CHILD | `AFTER ]
161
162 type tree_line_style = "GTK_CTREE_LINES_"
163   [ `NONE | `SOLID | `DOTTED | `TABBED ]
164
165 type tree_expander_style = "GTK_CTREE_EXPANDER_"
166   [ `NONE | `SQUARE | `TRIANGLE | `CIRCULAR ]
167
168 type tree_expansion_type = "GTK_CTREE_EXPANSION_"
169   [ `EXPAND | `EXPAND_RECURSIVE | `COLLAPSE | `COLLAPSE_RECURSIVE
170   | `TOGGLE | `TOGGLE_RECURSIVE ]
171 *)