X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2Fgtk.ml;fp=helm%2FDEVEL%2Flablgtk%2Flablgtk_20001129-0.1.0%2Fgtk.ml;h=0000000000000000000000000000000000000000;hp=0c7892e6f02e6398b5b815a69d0bacdcfd51e4fc;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gtk.ml b/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gtk.ml deleted file mode 100644 index 0c7892e6f..000000000 --- a/helm/DEVEL/lablgtk/lablgtk_20001129-0.1.0/gtk.ml +++ /dev/null @@ -1,158 +0,0 @@ -(* $Id$ *) - -exception Error of string -exception Warning of string -exception Cannot_cast of string * string -type 'a obj -type 'a optobj = 'a obj Gpointer.optboxed -type clampf = float - -module Tags = struct - type arrow_type = [ `UP|`DOWN|`LEFT|`RIGHT ] - type attach_options = [ `EXPAND|`SHRINK|`FILL ] - type direction_type = [ `TAB_FORWARD|`TAB_BACKWARD|`UP|`DOWN|`LEFT|`RIGHT ] - type justification = [ `LEFT|`RIGHT|`CENTER|`FILL ] - type match_type = [ `ALL|`ALL_TAIL|`HEAD|`TAIL|`EXACT|`LAST ] - type metric_type = [ `PIXELS|`INCHES|`CENTIMETERS ] - type orientation = [ `HORIZONTAL|`VERTICAL ] - type corner_type = [ `TOP_LEFT|`BOTTOM_LEFT|`TOP_RIGHT|`BOTTOM_RIGHT ] - type pack_type = [ `START|`END ] - type path_type = [ `WIDGET|`WIDGET_CLASS|`CLASS ] - type policy_type = [ `ALWAYS|`AUTOMATIC|`NEVER ] - type position = [ `LEFT|`RIGHT|`TOP|`BOTTOM ] - type preview_type = [ `COLOR|`GRAYSCALE ] - type relief_style = [ `NORMAL|`HALF|`NONE ] - type resize_mode = [ `PARENT|`QUEUE|`IMMEDIATE ] - type signal_run_type = [ `FIRST|`LAST|`BOTH|`NO_RECURSE|`ACTION|`NO_HOOKS ] - type scroll_type = - [ `NONE|`STEP_FORWARD|`STEP_BACKWARD|`PAGE_BACKWARD|`PAGE_FORWARD|`JUMP ] - type selection_mode = [ `SINGLE|`BROWSE|`MULTIPLE|`EXTENDED ] - type shadow_type = [ `NONE|`IN|`OUT|`ETCHED_IN|`ETCHED_OUT ] - type state_type = [ `NORMAL|`ACTIVE|`PRELIGHT|`SELECTED|`INSENSITIVE ] - type submenu_direction = [ `LEFT|`RIGHT ] - type submenu_placement = [ `TOP_BOTTOM|`LEFT_RIGHT ] - type toolbar_style = [ `ICONS|`TEXT|`BOTH ] - type trough_type = [ `NONE|`START|`END|`JUMP ] - type update_type = [ `CONTINUOUS|`DISCONTINUOUS|`DELAYED ] - type visibility = [ `NONE|`PARTIAL|`FULL ] - type window_position = [ `NONE|`CENTER|`MOUSE|`CENTER_ALWAYS ] - type window_type = [ `TOPLEVEL|`DIALOG|`POPUP ] - type sort_type = [ `ASCENDING|`DESCENDING ] - type fundamental_type = - [ `INVALID|`NONE|`CHAR|`BOOL|`INT|`UINT|`LONG|`ULONG|`FLOAT|`DOUBLE - |`STRING|`ENUM|`FLAGS|`BOXED|`FOREIGN|`CALLBACK|`ARGS|`POINTER - |`SIGNAL|`C_CALLBACK|`OBJECT ] - - type accel_flag = [ `VISIBLE|`SIGNAL_VISIBLE|`LOCKED ] - type button_box_style = [ `DEFAULT_STYLE|`SPREAD|`EDGE|`START|`END ] - type expand_type = [ `X|`Y|`BOTH|`NONE ] - type packer_options = [ `PACK_EXPAND|`FILL_X|`FILL_Y ] - type side_type = [ `TOP|`BOTTOM|`LEFT|`RIGHT ] - type anchor_type = [ `CENTER|`NORTH|`NW|`NE|`SOUTH|`SW|`SE|`WEST|`EAST ] - type update_policy = [ `ALWAYS|`IF_VALID|`SNAP_TO_TICKS ] - type cell_type = [ `EMPTY|`TEXT|`PIXMAP|`PIXTEXT|`WIDGET ] - type button_action = [ `SELECTS|`DRAGS|`EXPANDS ] - type calendar_display_options = - [ `SHOW_HEADING|`SHOW_DAY_NAMES|`NO_MONTH_CHANGE|`SHOW_WEEK_NUMBERS - |`WEEK_START_MONDAY ] - type spin_button_update_policy = [ `ALWAYS|`IF_VALID ] - type spin_type = - [ `STEP_FORWARD|`STEP_BACKWARD|`PAGE_FORWARD|`PAGE_BACKWARD - |`HOME|`END|`USER_DEFINED of float ] - type progress_bar_style = [ `CONTINUOUS|`DISCRETE ] - type progress_bar_orientation = - [ `LEFT_TO_RIGHT|`RIGHT_TO_LEFT|`BOTTOM_TO_TOP|`TOP_TO_BOTTOM ] - type dest_defaults = [ `MOTION|`HIGHLIGHT|`DROP|`ALL ] - type target_flags = [ `SAME_APP|`SAME_WIDGET ] - type font_metric_type = [ `PIXELS|`POINTS ] - type font_type = [ `BITMAP|`SCALABLE|`SCALABLE_BITMAP|`ALL ] - type font_filter_type = [ `BASE|`USER ] -end -open Tags - -type gtk_type -type gtk_class - -type accel_group - -type style -type 'a group = 'a obj option - -type statusbar_message -type statusbar_context - -type color = { red: float; green: float; blue: float; opacity: float } -type rectangle = { x: int; y: int; width: int; height: int } -type target_entry = { target: string; flags: target_flags list; info: int } - -type data = [`data] -type adjustment = [`data|`adjustment] -type tooltips = [`data|`tooltips] -type widget = [`widget] -type container = [`widget|`container] -type alignment = [`widget|`container|`bin|`alignment] -type event_box = [`widget|`container|`bin|`eventbox] -type frame = [`widget|`container|`bin|`frame] -type aspect_frame = [`widget|`container|`bin|`frame|`aspect] -type handle_box = [`widget|`container|`bin|`handlebox] -type invisible = [`widget|`container|`bin|`invisible] -type item = [`widget|`container|`bin|`item] -type list_item = [`widget|`container|`bin|`item|`listitem] -type menu_item = [`widget|`container|`bin|`item|`menuitem] -type check_menu_item = [`widget|`container|`bin|`item|`menuitem|`checkmenuitem] -type radio_menu_item = - [`widget|`container|`bin|`item|`menuitem|`checkmenuitem|`radiomenuitem] -type tree_item = [`widget|`container|`bin|`item|`treeitem] -type viewport = [`widget|`container|`bin|`viewport] -type window = [`widget|`container|`bin|`window] -type color_selection_dialog = [`widget|`container|`window|`colorseldialog] -type dialog = [`widget|`container|`bin|`window|`dialog] -type input_dialog = [`widget|`container|`bin|`window|`dialog|`inputdialog] -type file_selection = [`widget|`container|`bin|`window|`filesel] -type font_selection_dialog = [`widget|`container|`bin|`window|`fontseldialog] -type plug = [`widget|`container|`bin|`window|`plug] -type box = [`widget|`container|`box] -type button_box = [`widget|`container|`box|`bbox] -type gamma_curve = [`widget|`container|`bbox|`gamma] -type color_selection = [`widget|`container|`box|`colorsel] -type combo = [`widget|`container|`box|`combo] -type statusbar = [`widget|`container|`box|`statusbar] -type button = [`widget|`container|`button] -type toggle_button = [`widget|`container|`button|`toggle] -type radio_button = [`widget|`container|`button|`toggle|`radio] -type option_menu = [`widget|`container|`button|`optionmenu] -type clist = [`widget|`container|`clist] -type fixed = [`widget|`container|`fixed] -type layout = [`widget|`container|`layout] -type liste = [`widget|`container|`list] -type menu_shell = [`widget|`container|`menushell] -type menu = [`widget|`container|`menushell|`menu] -type menu_bar = [`widget|`container|`menushell|`menubar] -type notebook = [`widget|`container|`notebook] -type font_selection = [`widget|`container|`notebook|`fontsel] -type packer = [`widget|`container|`packer] -type paned = [`widget|`container|`paned] -type scrolled_window = [`widget|`container|`scrolled] -type socket = [`widget|`container|`socket] -type table = [`widget|`container|`table] -type toolbar = [`widget|`container|`toolbar] -type tree = [`widget|`container|`tree] -type calendar = [`widget|`calendar] -type drawing_area = [`widget|`drawing] -type editable = [`widget|`editable] -type entry = [`widget|`editable|`entry] -type spin_button = [`widget|`editable|`entry|`spinbutton] -type text = [`widget|`editable|`text] -type misc = [`widget|`misc] -type arrow = [`widget|`misc|`arrow] -type image = [`widget|`misc|`image] -type label = [`widget|`misc|`label] -type tips_query = [`widget|`misc|`label|`tipsquery] -type pixmap = [`widget|`misc|`pixmap] -type progress = [`widget|`progress] -type progress_bar = [`widget|`progress|`progressbar] -type range = [`widget|`range] -type scale = [`widget|`range|`scale] -type scrollbar = [`widget|`range|`scrollbar] -type ruler = [`widget|`ruler] -type separator = [`widget|`separator]