## tk_types.pkg
## Author: cxl (Last modification by $Author: 2cxl $)
## (C) 1996, Bremen Institute for Safe Systems, Universitaet Bremen
# Compiled by:
# src/lib/tk/src/tk.sublib# ***************************************************************************
#
# tk Export API. ``All you ever wanted to know about tk''
#
# Part I: Types, type constructors, selectors etc.
#
# $Date: 2001/03/30 13:39:21 $
# $Revision: 3.0 $
#
# **************************************************************************
api Tk_Types {
/* Exceptions:
*/
exception CANVAS_ITEM String;
exception WIDGET String;
exception TCL_ERROR String;
exception CONFIG String;
exception WINDOWS String;
Text_Item_Id;
Title;
Widget_Path;
# All these should be paths, as in winix__premicrothread::path
Bitmap_Name = String;
# Pixmap_File;
Cursor_Name = String;
Bitmap_File = String;
Image_File = String;
Cursor_File = String;
# Identifiers for tk's entities: windows, CItems, Images, Widgets
eqtype Window_Id;
eqtype Canvas_Item_Id;
eqtype Image_Id;
eqtype Widget_Id;
Coordinate = (Int, Int);
Tk_Event
=
TK_EVENT (Int, # %b Button number
String, # %s state field
Int, # %x x field
Int, # %y y field
Int, # %X x_root field
Int); # %Y y_root field
# -- selectors
get_button: Tk_Event -> Int;
get_state: Tk_Event -> String;
get_x_coordinate: Tk_Event -> Int;
get_root_x_coordinate: Tk_Event -> Int;
get_y_coordinate: Tk_Event -> Int;
get_root_y_coordinate: Tk_Event -> Int;
Void_Callback = Void -> Void;
Real_Callback = Float -> Void;
Callback = Tk_Event -> Void;
Event =
# window events
FOCUS_IN
| FOCUS_OUT
| CONFIGURE
| MAP
| UNMAP
| VISIBILITY
| DESTROY
# Key press/release events
| KEY_PRESS String
| KEY_RELEASE String
# Button press/release events, NULL means any old Button
| BUTTON_PRESS null_or::Null_Or( Int )
| BUTTON_RELEASE null_or::Null_Or( Int )
# Cursor events
| ENTER | LEAVE | MOTION
# user-defined events, or explicitly given events
| DEPRECATED_EVENT String
# event modifiers
| SHIFT Event | CONTROL Event | LOCK Event | ANY Event
| DOUBLE Event | TRIPLE Event
| MODIFIER_BUTTON (Int, Event)
| ALT Event | META Event
| MOD3 Event | MOD4 Event | MOD5 Event;
# Not all combinations make sense, eg.
# modifiying a Button event with a different Button will cast
# doubt on either your sanity or understanding of these events
Event_Callback
=
EVENT_CALLBACK (Event, Callback);
Relief_Kind
=
FLAT | GROOVE | RAISED | RIDGE | SUNKEN;
Color
=
NO_COLOR | BLACK | WHITE | GREY | BLUE | GREEN | RED | BROWN | YELLOW
| PURPLE | ORANGE | MIX { red: Int, blue: Int, green: Int };
Arrowhead_Pos
=
ARROWHEAD_NONE | ARROWHEAD_FIRST | ARROWHEAD_LAST | ARROWHEAD_BOTH;
Capstyle_Kind
=
BUTT | PROJECTING | ROUND;
Joinstyle_Kind
=
BEVEL | MITER | ROUNDJOIN;
Anchor_Kind
=
NORTH | NORTHEAST |
EAST | SOUTHEAST |
SOUTH | SOUTHWEST |
WEST | NORTHWEST |
CENTER;
Icon_Variety
=
NO_ICON
| TK_BITMAP Bitmap_Name # -bitmap <tk bitmap>
| FILE_BITMAP Bitmap_File # -bitmap @<filename>
# | FILE_PIXMAP (Pixmap_File, Image_ID)
| FILE_IMAGE (Image_File, Image_Id);
Cursor_Kind
=
NO_CURSOR
| XCURSOR (Cursor_Name, (Null_Or( (Color, Null_Or( Color )) ) ))
| FILE_CURSOR (Cursor_File, Color, (Null_Or( (Cursor_File, Color) ) ));
Justify = JUSTIFY_LEFT | JUSTIFY_RIGHT | JUSTIFY_CENTER;
Wrap_Mode = NO_WRAP | WRAP_CHAR | WRAP_WORD;
Font_Trait
=
BOLD | ITALIC
| TINY | SMALL | NORMAL_SIZE | LARGE | HUGE
| SCALE Float;
Font
=
XFONT String
| NORMAL_FONT List( Font_Trait )
| TYPEWRITER List( Font_Trait )
| SANS_SERIF List( Font_Trait )
| SYMBOL List( Font_Trait );
Color_Mode
=
PRINTCOLOR | PRINTGREY | PRINTMONO;
Colormap_Entry
=
COLORMAP_ENTRY (String, String, String, String);
Fontmap_Entry
=
FONTMAP_ENTRY (String, String, Int);
Orientation
=
HORIZONTAL | VERTICAL;
Trait
=
WIDTH Int
| HEIGHT Int
| BORDER_THICKNESS Int
| RELIEF Relief_Kind
| FOREGROUND Color
| BACKGROUND Color
| MENU_UNDERLINE Int # -underline ... for menus
| ACCELERATOR String # -accelerator "bla"
| TEXT String # -Label "bla"
| FONT Font # -font "bla"
| VARIABLE String # -variable "bla"
| VALUE String # -value "bla"
| ICON Icon_Variety # -bitmap or -image ...
| CURSOR Cursor_Kind # -cursor ...
| CALLBACK Void_Callback
| ANCHOR Anchor_Kind
# Configuration options for tags in text widgets
| FILL_COLOR Color
| OUTLINE Color
| OFFSET Int
| UNDERLINE
| JUSTIFY Justify
| WRAP Wrap_Mode
| OUTLINE_WIDTH Int
# | STIPPLE
| SMOOTH Bool
| ARROW Arrowhead_Pos
| SCROLL_REGION (Int, Int, Int, Int)
| CAP_STYLE Capstyle_Kind
| JOIN_STYLE Joinstyle_Kind
| COLOR_MAP List( Colormap_Entry )
| COLOR_MODE Color_Mode
| FILE String
| FONT_MAP List( Fontmap_Entry )
| PRINT_HEIGHT String
| PAGE_ANCHOR Anchor_Kind
| PAGE_HEIGHT String
| PAGE_WIDTH String
| PAGE_X String
| PAGE_Y String
| ROTATE Bool
| PRINT_WIDTH String
| PRINT_X String
| PRINT_Y String
| ORIENT Orientation
| SLIDER_LABEL String
| LENGTH Int
| SLIDER_LENGTH Int
| FROM Float
| TO Float
| RESOLUTION Float
| DIGITS Int
| BIG_INCREMENT Float
| TICK_INTERVAL Float
| SHOW_VALUE Bool
| SLIDER_RELIEF Relief_Kind
| ACTIVE Bool
| REAL_CALLBACK Real_Callback
| REPEAT_DELAY Int
| REPEAT_INTERVAL Int
| THROUGH_COLOR Color
| INNER_PAD_X Int
| INNER_PAD_Y Int
| SHOW Char
| TEAR_OFF Bool;
User_Kind
=
USER
| PROGRAM;
Window_Trait
=
WINDOW_ASPECT_RATIO_LIMITS (Int, Int, Int, Int) # xthin/ythin xfat/yfat
| WIDE_HIGH_X_Y ((null_or::Null_Or ((Int, Int))), # width x height
(null_or::Null_Or ((Int, Int)))) # xpos x ypos
/*
| WINDOW_ICON of Icon_Variety
| WINDOW_ICON_MASK of Icon_Variety
| WINDOW_ICON_NAME of String
*/
| WIDE_HIGH_MAX (Int, Int) # width * height
| WIDE_HIGH_MIN (Int, Int)
| WINDOW_POSITIONED_BY User_Kind
| WINDOW_SIZED_BY User_Kind
| WINDOW_TITLE String
| WINDOW_GROUP Window_Id # window / leader
| TRANSIENTS_LEADER Window_Id null_or::Null_Or # Mark window as popup, optionally give parent window.
| OMIT_WINDOW_MANAGER_DECORATIONS Bool;
Edge
=
TOP | BOTTOM | LEFT | RIGHT;
Fill_Style
=
ONLY_X | ONLY_Y | XY;
# Stick to which sides of grid cell? (GRIDDED packer only.)
Sticky_Kind
=
TO_N | TO_S | TO_E | TO_W | TO_NS | TO_NE | TO_NW | TO_SE | TO_SW | TO_EW | TO_NSE | TO_NSW | TO_NEW | TO_SEW | TO_NSEW;
Scrollbars_At
=
NOWHERE | AT_LEFT | AT_RIGHT | AT_TOP | AT_BOTTOM
| AT_LEFT_AND_TOP | AT_RIGHT_AND_TOP | AT_LEFT_AND_BOTTOM | AT_RIGHT_AND_BOTTOM;
Packing_Hint
=
EXPAND Bool
| FILL Fill_Style
| PAD_X Int
| PAD_Y Int
| PACK_AT Edge
| COLUMN Int
| ROW Int
| STICK Sticky_Kind;
Mark =
MARK (Int, # line number [1..]
Int) # Char number [0..]
| MARK_TO_END Int # end of line i
| MARK_END; # end of text
# main sumtypes: widgets, text text_items, Canvas items, menu items
Menu_Item
=
MENU_CHECKBUTTON List( Trait )
| MENU_RADIOBUTTON List( Trait )
| MENU_COMMAND List( Trait )
| MENU_CASCADE (List( Menu_Item ), List( Trait ))
| MENU_SEPARATOR;
Canvas_Item
=
CANVAS_BOX { citem_id: Canvas_Item_Id, coord1: Coordinate, coord2: Coordinate, traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_OVAL { citem_id: Canvas_Item_Id, coord1: Coordinate, coord2: Coordinate, traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_LINE { citem_id: Canvas_Item_Id, coords: List( Coordinate ), traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_POLYGON { citem_id: Canvas_Item_Id, coords: List( Coordinate ), traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_TEXT { citem_id: Canvas_Item_Id, coord: Coordinate, traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_ICON { citem_id: Canvas_Item_Id, coord: Coordinate, icon_variety: Icon_Variety, traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_WIDGET { citem_id: Canvas_Item_Id, coord: Coordinate, subwidgets: Widgets, traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS_TAG { citem_id: Canvas_Item_Id, citem_ids: List( Canvas_Item_Id ) }
also Live_Text =
LIVE_TEXT { len: null_or::Null_Or( (Int, Int) ), str: String,
text_items: List( Text_Item ) }
also Text_Item
=
TEXT_ITEM_TAG { text_item_id: Text_Item_Id, marks: List( (Mark, Mark) ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| TEXT_ITEM_WIDGET { text_item_id: Text_Item_Id, mark: Mark, subwidgets: Widgets,
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
also Widget
= FRAME { widget_id: Widget_Id, subwidgets: Widgets, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| MESSAGE { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| LABEL { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| LIST_BOX { widget_id: Widget_Id, scrollbars: Scrollbars_At,
packing_hints: List( Packing_Hint ), traits: List( Trait ),
event_callbacks: List( Event_Callback ) }
| BUTTON { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| RADIO_BUTTON { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CHECK_BUTTON { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| MENU_BUTTON { widget_id: Widget_Id, mitems: List( Menu_Item ),
packing_hints: List( Packing_Hint ), traits: List( Trait ),
event_callbacks: List( Event_Callback ) }
| TEXT_ENTRY { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| TEXT_WIDGET { widget_id: Widget_Id, scrollbars: Scrollbars_At,
live_text: Live_Text, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| CANVAS { widget_id: Widget_Id, scrollbars: Scrollbars_At,
citems: List( Canvas_Item ), packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
| POPUP { widget_id: Widget_Id, traits: List( Trait ),
mitems: List( Menu_Item ) }
| SCALE_WIDGET { widget_id: Widget_Id, packing_hints: List( Packing_Hint ),
traits: List( Trait ), event_callbacks: List( Event_Callback ) }
also Widgets
=
PACKED List( Widget )
| GRIDDED List( Widget );
# -- selectors for all widgets
get_widget_id: Widget -> Widget_Id;
get_widget_event_callbacks: Widget -> List( Event_Callback );
get_widget_traits: Widget -> List( Trait );
get_widget_packing_hints: Widget -> List( Packing_Hint );
# -- update functions for all widgets
update_widget_event_callbacks: Widget -> List( Event_Callback ) -> Widget;
update_widget_traits: Widget -> List ( Trait ) -> Widget;
update_widget_packing_hints: Widget -> List( Packing_Hint ) -> Widget;
# -- selector for frames: get all subwidgets
get_subwidgets: Widget -> List( Widget );
# -- selectors for Canvas widgets
get_canvas_items: Widget -> List( Canvas_Item );
get_canvas_scrollbars: Widget -> Scrollbars_At;
# -- update functions for Canvas Widgets
update_canvas_items: Widget -> List( Canvas_Item ) -> Widget;
update_canvas_scrollbars: Widget -> Scrollbars_At -> Widget;
# -- selectors for Text widgets
get_text_widget_scrollbars: Widget -> Scrollbars_At;
get_text_widget_livetext: Widget -> Live_Text;
get_text_widget_text: Widget -> String;
get_text_widget_text_items: Widget -> List( Text_Item );
update_text_widget_scrollbars: Widget -> Scrollbars_At -> Widget;
update_text_widget_annotations: Widget -> List( Text_Item ) -> Widget;
# -- selectors for Canvas_Item
get_canvas_item_id: Canvas_Item -> Canvas_Item_Id;
get_canvas_item_coordinates: Canvas_Item -> List( Coordinate );
get_canvas_item_traits: Canvas_Item -> List( Trait );
get_canvas_item_event_callbacks: Canvas_Item -> List( Event_Callback );
get_canvas_item_icon: Canvas_Item -> Icon_Variety;
get_canvas_item_canvas_items: Canvas_Item -> List( Canvas_Item_Id );
get_canvas_item_subwidgets: Canvas_Item -> List( Widget );
# -- update functions for Canvas_Item
update_canvas_item_coordinates: Canvas_Item -> List( Coordinate ) -> Canvas_Item;
update_canvas_item_traits: Canvas_Item -> List( Trait ) -> Canvas_Item;
update_canvas_item_event_callbacks: Canvas_Item -> List( Event_Callback ) -> Canvas_Item;
update_canvas_item_icon: Canvas_Item -> Icon_Variety -> Canvas_Item;
update_canvas_item_canvas_items: Canvas_Item -> List( Canvas_Item_Id ) -> Canvas_Item;
update_canvas_item_subwidgets: Canvas_Item -> List( Widget ) -> Canvas_Item;
# -- selectors and update function for Live_Text
get_livetext_text: Live_Text -> String;
get_livetext_text_items: Live_Text -> List( Text_Item );
update_livetext_text_items: Live_Text -> List( Text_Item ) -> Live_Text;
get_livetext_rows_cols: Live_Text -> { rows: Int, cols: Int };
# -- selectors for Text_Item
get_text_item_id: Text_Item -> Text_Item_Id;
get_text_item_traits: Text_Item -> List( Trait );
get_text_item_event_callbacks: Text_Item -> List( Event_Callback );
get_text_item_marks: Text_Item -> List ((Mark, Mark));
get_text_widget_subwidgets: Text_Item -> List( Widget );
# -- update functions for Text_Item
update_text_item_traits: Text_Item -> List( Trait ) -> Text_Item;
update_text_item_event_callbacks: Text_Item -> List( Event_Callback ) -> Text_Item;
update_text_item_subwidgets: Text_Item -> List( Widget ) -> Text_Item;
# -- selectors for Menu_Item
get_menu_item_callback: Menu_Item -> Void_Callback;
get_menu_item_relief_kind: Menu_Item -> Relief_Kind;
get_menu_item_text: Menu_Item -> String;
get_menu_item_width: Menu_Item -> Int;
get_menu_item_traits: Menu_Item -> List( Trait );
Window
# -- selectors
; get_window_callback: Window -> Void_Callback;
get_window_event_callbacks: Window -> List( Event_Callback );
get_window_traits: Window -> List( Window_Trait );
get_window_subwidgets: Window -> List( Widget );
get_window_id: Window -> Window_Id;
window_is_gridded: Window -> Bool;
};
package tk_types
: (weak) Tk_Types # Tk_Types is from src/lib/tk/src/tk_types.pkg{
include package fonts;
include package basic_tk_types;
include package config;
include package canvas_item;
include package text_item;
include package live_text;
include package tk_event;
include package com_state;
Text_Item_Id = String;
Title = String;
Widget_Path = String;
Bitmap_Name = String;
Bitmap_File = String;
Image_File = String;
Pixmap_File = String;
Cursor_Name = String;
Cursor_File = String;
Coordinate = (Int, Int);
# Canvas_Item
get_canvas_item_traits = sel_item_configure;
get_canvas_item_event_callbacks = sel_item_naming;
update_canvas_item_traits = upd_item_configure;
update_canvas_item_event_callbacks = upd_item_naming;
# text_item
get_text_item_traits = sel_annotation_configure;
get_text_item_event_callbacks = sel_annotation_naming;
update_text_item_traits = upd_annotation_configure;
update_text_item_event_callbacks = upd_annotation_naming;
/* Widget */
get_widget_id = get_widget_id;
get_widget_traits = get_the_widget_traits;
get_widget_event_callbacks = get_the_widget_event_callbacks;
get_widget_packing_hints = get_the_widget_packing_hints;
sel_widget_type = get_widget_type;
update_widget_traits = set_the_widget_traits;
update_widget_packing_hints = set_the_widget_packing_hints;
update_widget_event_callbacks = set_the_widget_event_callbacks;
# FRAME
fun get_subwidgets (FRAME { subwidgets=> ws, ... } )
=
get_raw_widgets ws;
Window = (Window_Id, List( Window_Trait ), Widgets, List( Event_Callback ) ,
Void_Callback);
};