X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fgtk_tags.var;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20000829-0.1.0%2Fgtk_tags.var;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=eb4ead78d061ccfa9793bdbe25495f303bcf3f73;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gtk_tags.var b/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gtk_tags.var deleted file mode 100644 index eb4ead78d..000000000 --- a/helm/DEVEL/lablgtk/lablgtk_20000829-0.1.0/gtk_tags.var +++ /dev/null @@ -1,171 +0,0 @@ -(* $Id$ *) - -exception ml_raise_gtk - -type arrow_type = "GTK_ARROW_" - [ `UP | `DOWN | `LEFT | `RIGHT ] - -type attach_options = "GTK_" - [ `EXPAND | `SHRINK | `FILL ] - -type button_box_style = "GTK_BUTTONBOX_" - [ `DEFAULT_STYLE | `SPREAD | `EDGE | `START | `END ] - -type direction_type = "GTK_DIR_" - [ `TAB_FORWARD | `TAB_BACKWARD | `UP | `DOWN | `LEFT | `RIGHT ] - -type justification = "GTK_JUSTIFY_" - [ `LEFT | `RIGHT | `CENTER | `FILL ] - -type match_type = "GTK_MATCH_" - [ `ALL | `ALL_TAIL | `HEAD | `TAIL | `EXACT | `LAST ] - -type metric_type = "GTK_" - [ `PIXELS | `INCHES | `CENTIMETERS ] - -type orientation = "GTK_ORIENTATION_" - [ `HORIZONTAL | `VERTICAL ] - -type corner_type = "GTK_CORNER_" - [ `TOP_LEFT | `BOTTOM_LEFT | `TOP_RIGHT | `BOTTOM_RIGHT ] - -type pack_type = "GTK_PACK_" - [ `START | `END ] - -type path_type = "GTK_PATH_" - [ `WIDGET | `WIDGET_CLASS | `CLASS ] - -type policy_type = "GTK_POLICY_" - [ `ALWAYS | `AUTOMATIC | `NEVER ] - -type position = "GTK_POS_" - [ `LEFT | `RIGHT | `TOP | `BOTTOM ] - -type preview_type = "GTK_PREVIEW_" - [ `COLOR | `GRAYSCALE ] - -type relief_style = "GTK_RELIEF_" - [ `NORMAL | `HALF | `NONE ] - -type resize_mode = "GTK_RESIZE_" - [ `PARENT | `QUEUE | `IMMEDIATE ] - -type signal_run_type = "GTK_RUN_" - [ `FIRST | `LAST | `BOTH | `NO_RECURSE | `ACTION | `NO_HOOKS ] - -type scroll_type = "GTK_SCROLL_" - [ `NONE | `STEP_FORWARD | `STEP_BACKWARD | `PAGE_BACKWARD - | `PAGE_FORWARD | `JUMP ] - -type selection_mode = "GTK_SELECTION_" - [ `SINGLE | `BROWSE | `MULTIPLE | `EXTENDED ] - -type shadow_type = "GTK_SHADOW_" - [ `NONE | `IN | `OUT | `ETCHED_IN | `ETCHED_OUT ] - -type state_type = "GTK_STATE_" - [ `NORMAL | `ACTIVE | `PRELIGHT | `SELECTED | `INSENSITIVE ] - -type submenu_direction = "GTK_DIRECTION_" - [ `LEFT | `RIGHT ] - -type submenu_placement = "GTK_" - [ `TOP_BOTTOM | `LEFT_RIGHT ] - -type toolbar_style = "GTK_TOOLBAR_" - [ `ICONS | `TEXT | `BOTH ] - -type trough_type = "GTK_TROUGH_" - [ `NONE | `START | `END | `JUMP ] - -type update_type = "GTK_UPDATE_" - [ `CONTINUOUS | `DISCONTINUOUS | `DELAYED ] - -type visibility = "GTK_VISIBILITY_" - [ `NONE | `PARTIAL | `FULL ] - -type window_position = "GTK_WIN_POS_" - [ `NONE | `CENTER | `MOUSE | `CENTER_ALWAYS ] - -type window_type = "GTK_WINDOW_" - [ `TOPLEVEL | `DIALOG | `POPUP ] - -type sort_type = "GTK_SORT_" - [ `ASCENDING | `DESCENDING ] - - -type fundamental_type = "GTK_TYPE_" - [ `INVALID | `NONE | `CHAR | `BOOL | `INT | `UINT | `LONG | `ULONG - | `FLOAT | `DOUBLE | `STRING | `ENUM | `FLAGS | `BOXED | `FOREIGN - | `CALLBACK | `ARGS | `POINTER | `SIGNAL | `C_CALLBACK | `OBJECT ] - -type cell_type = "GTK_CELL_" - [ `EMPTY | `TEXT | `PIXMAP | `PIXTEXT | `WIDGET ] - -type toolbar_child = "GTK_TOOLBAR_CHILD_" - [ `SPACE | `BUTTON | `TOGGLEBUTTON | `RADIOBUTTON | `WIDGET ] - -type toolbar_space_style = "GTK_TOOLBAR_SPACE_" - [ `EMPTY | `LINE ] - -type tree_view_mode = "GTK_TREE_VIEW_" - [ `LINE | `ITEM ] - -type spin_type = "GTK_SPIN_" - [ `STEP_FORWARD | `STEP_BACKWARD | `PAGE_FORWARD | `PAGE_BACKWARD - | `HOME | `END | `USER_DEFINED ] - -type accel_flag = "GTK_ACCEL_" - [ `VISIBLE | `SIGNAL_VISIBLE | `LOCKED ] - -type packer_options = "GTK_" - [ `PACK_EXPAND | `FILL_X | `FILL_Y ] - -type side_type = "GTK_SIDE_" - [ `TOP | `BOTTOM | `LEFT | `RIGHT ] - -type anchor_type = "GTK_ANCHOR_" - [ `CENTER | `NORTH | `NW | `NE | `SOUTH | `SW | `SE | `WEST | `EAST ] - -type button_action = "GTK_BUTTON_" - [ `SELECTS | `DRAGS | `EXPANDS ] - -type calendar_display_options = "GTK_CALENDAR_" - [ `SHOW_HEADING | `SHOW_DAY_NAMES | `NO_MONTH_CHANGE | `SHOW_WEEK_NUMBERS - | `WEEK_START_MONDAY ] - -type progress_bar_style = "GTK_PROGRESS_" - [ `CONTINUOUS | `DISCRETE ] - -type progress_bar_orientation = "GTK_PROGRESS_" - [ `LEFT_TO_RIGHT | `RIGHT_TO_LEFT | `BOTTOM_TO_TOP | `TOP_TO_BOTTOM ] - -type dest_defaults = "GTK_DEST_DEFAULT_" - [ `MOTION | `HIGHLIGHT | `DROP | `ALL ] - -type target_flags = "GTK_TARGET_" - [ `SAME_APP | `SAME_WIDGET ] - -type font_metric_type = "GTK_FONT_METRIC_" - [ `PIXELS | `POINTS ] - -type font_type = "GTK_FONT_" - [ `BITMAP | `SCALABLE | `SCALABLE_BITMAP | `ALL ] - -type font_filter_type = "GTK_FONT_FILTER_" - [ `BASE | `USER ] - -(* -type tree_pos = "GTK_CTREE_POS_" - [ `BEFORE | `AS_CHILD | `AFTER ] - -type tree_line_style = "GTK_CTREE_LINES_" - [ `NONE | `SOLID | `DOTTED | `TABBED ] - -type tree_expander_style = "GTK_CTREE_EXPANDER_" - [ `NONE | `SQUARE | `TRIANGLE | `CIRCULAR ] - -type tree_expansion_type = "GTK_CTREE_EXPANSION_" - [ `EXPAND | `EXPAND_RECURSIVE | `COLLAPSE | `COLLAPSE_RECURSIVE - | `TOGGLE | `TOGGLE_RECURSIVE ] -*)