## basic-tk-types.pkg
## Author: bu
## (C) 1996, Bremen Institute for Safe Systems, Universitaet Bremen
# Compiled by:
# src/lib/tk/src/tk.sublib# Basic Data Structures for tk
#
package basic_tk_types {
Void_Callback = Void -> Void;
Real_Callback = Float -> Void;
Widget_Path = String;
Tcl_Path = String;
Widget_Id = String;
Window_Path = String;
Window_Id = String;
Title = String;
Text_Item_Id = String;
Int_Path = ((Window_Id, Widget_Path));
Path_Ass = ((Widget_Id, Int_Path));
Canvas_Item_Id = String;
Coordinate = ((Int, Int));
Bitmap_Name = String;
Bitmap_File = String;
Image_File = String;
Image_Id = String;
# type Pixmap_File = String
Cursor_Name = String;
Cursor_File = String;
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
/*
TKEButtonPress of 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
| TKEUnspecified of
Int # %x x field
* Int # %y y field
*/
Callback = Tk_Event -> Void;
Event
= 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::Null_Or ((Color, (null_or::Null_Or Color)))))
| FILE_CURSOR (Cursor_File, Color, (null_or::Null_Or ((Cursor_File, Color))));
Color_Mode = PRINTCOLOR | PRINTGREY | PRINTMONO;
Colormap_Entry = COLORMAP_ENTRY (String, String, String, String);
Fontmap_Entry
=
FONTMAP_ENTRY (String, String, Int);
Justify
=
JUSTIFY_LEFT | JUSTIFY_RIGHT | JUSTIFY_CENTER;
Wrap_Mode = NO_WRAP | WRAP_CHAR | WRAP_WORD;
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 fonts::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
| FILL_COLOR Color
| OUTLINE Color
| 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
| OFFSET Int # Offset over baseline for texts
| UNDERLINE # underline for texts (see MUnderline above)
| JUSTIFY Justify # Justification: left/right/center
| WRAP Wrap_Mode
| 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
# | WinIcon of Icon_Variety
# | WinIconMask of Icon_Variety
# | WinIconName 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 null_or::Null_Or( Window_Id )
| OMIT_WINDOW_MANAGER_DECORATIONS Bool;
Edge = TOP | BOTTOM | LEFT | RIGHT;
Fill_Style = ONLY_X | ONLY_Y | XY;
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, Int)
| MARK_TO_END Int
| MARK_END;
Menu_Item =
MENU_CHECKBUTTON List( Trait )
| MENU_RADIOBUTTON List( Trait )
| MENU_COMMAND List( Trait )
| MENU_CASCADE (List( Menu_Item ), List( Trait ))
| MENU_SEPARATOR;
Text_Item_Type = TEXT_ITEM_TAG_TYPE | TEXT_ITEM_WIDGET_TYPE;
Canvas_Item_Type =
CANVAS_BOX_TYPE | CANVAS_OVAL_TYPE | CANVAS_LINE_TYPE | CANVAS_POLYGON_TYPE /* | CANVAS_ARC_TYPE */ | CANVAS_TEXT_TYPE
| CANVAS_ICON_TYPE | CANVAS_WIDGET_TYPE | CANVAS_TAG_TYPE;
Menu_Item_Type = CHECKBOX_MENU_ITEM_TYPE | RADIO_BUTTON_MENU_ITEM_TYPE | CASCADE_MENU_ITEM_TYPE | SEPARATOR_MENU_ITEM_TYPE | COMMAND_MENU_ITEM_TYPE;
Widget_Type =
FRAME_TYPE | MESSAGE_TYPE | LABEL_TYPE | LIST_BOX_TYPE | BUTTON_TYPE | CHECK_BUTTON_TYPE | RADIO_BUTTON_TYPE | SCALE_TYPE
| MENU_BUTTON_TYPE | TEXT_ENTRY_TYPE | CANVAS_TYPE | TEXT_WIDGET_TYPE | POPUP_TYPE;
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 (Widget List)
| GRIDDED (Widget List);
Window = (Window_Id, List( Window_Trait ), Widgets, List( Event_Callback ) ,
Void_Callback);
# *************************************************************************
#
# Initialization of the internal state
#
# *************************************************************************
/*
type GUI = (List (Window) * List( PathAss ))
gui_state = Ref( []: List( Window ),
[]: List( PathAss ),
[]: List( Tcl_Answer )
)
*/
Tcl_Answer = String;
Program_Name = String;
Program_Parameters = List( String );
Program = ((Program_Name, Program_Parameters));
Protocol_Name = String;
# *************************************************************************
#
# Exceptions
#
# *************************************************************************
exception CONFIG String;
exception WIDGET String;
exception WINDOWS String;
exception TCL_ERROR String;
# ******************************************************************
#
# Elementary Selectors and Tests
#
# ******************************************************************
fun get_window_id (a, _, _, _, _) = a;
fun get_window_traits (_, wc, _, _, _)
=
wc;
fun get_window_subwidgets (_, _, c, _, _)
=
case c
PACKED widgets => widgets;
GRIDDED widgets => widgets; esac;
fun get_raw_widgets (PACKED widgets) => widgets;
get_raw_widgets (GRIDDED widgets) => widgets; end;
fun is_gridded widgets
=
case widgets
PACKED _ => FALSE;
GRIDDED _ => TRUE; esac;
fun window_is_gridded (_, _, ws, _, _) = is_gridded ws;
fun get_window_event_callbacks (_, _, _, b, _) = b;
fun get_window_callback (_, _, _, _, d) = d;
fun update_window_traits (id, wc, c, b, d) wc' = (id, wc', c, b, d);
fun get_widget_id (FRAME { widget_id, ... } ) => widget_id;
get_widget_id (MESSAGE { widget_id, ... } ) => widget_id;
get_widget_id (LABEL { widget_id, ... } ) => widget_id;
get_widget_id (LIST_BOX { widget_id, ... } ) => widget_id;
get_widget_id (BUTTON { widget_id, ... } ) => widget_id;
get_widget_id (RADIO_BUTTON { widget_id, ... } ) => widget_id;
get_widget_id (CHECK_BUTTON { widget_id, ... } ) => widget_id;
get_widget_id (MENU_BUTTON { widget_id, ... } ) => widget_id;
get_widget_id (TEXT_WIDGET { widget_id, ... } ) => widget_id;
get_widget_id (CANVAS { widget_id, ... } ) => widget_id;
get_widget_id (POPUP { widget_id, ... } ) => widget_id;
get_widget_id (TEXT_ENTRY { widget_id, ... } ) => widget_id;
get_widget_id (SCALE_WIDGET { widget_id, ... } ) => widget_id; end;
fun get_widget_type (FRAME _) => FRAME_TYPE;
get_widget_type (MESSAGE _) => MESSAGE_TYPE;
get_widget_type (LABEL _) => LABEL_TYPE;
get_widget_type (LIST_BOX _) => LIST_BOX_TYPE;
get_widget_type (BUTTON _) => BUTTON_TYPE;
get_widget_type (RADIO_BUTTON _) => RADIO_BUTTON_TYPE;
get_widget_type (CHECK_BUTTON _) => CHECK_BUTTON_TYPE;
get_widget_type (MENU_BUTTON _) => MENU_BUTTON_TYPE;
get_widget_type (TEXT_WIDGET _) => TEXT_WIDGET_TYPE;
get_widget_type (CANVAS _) => CANVAS_TYPE;
get_widget_type (POPUP _) => POPUP_TYPE;
get_widget_type (TEXT_ENTRY _) => TEXT_ENTRY_TYPE;
get_widget_type (SCALE_WIDGET _) => SCALE_TYPE; end;
fun get_the_widget_event_callbacks (FRAME { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (MESSAGE { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (LABEL { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (LIST_BOX { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (BUTTON { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (RADIO_BUTTON { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (CHECK_BUTTON { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (MENU_BUTTON { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (TEXT_WIDGET { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (CANVAS { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (POPUP w) => [];
get_the_widget_event_callbacks (TEXT_ENTRY { event_callbacks, ... } ) => event_callbacks;
get_the_widget_event_callbacks (SCALE_WIDGET { event_callbacks, ... } ) => event_callbacks; end;
fun set_the_widget_event_callbacks (FRAME { widget_id, subwidgets, packing_hints, traits, event_callbacks } ) nb =>
FRAME { widget_id, subwidgets, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (MESSAGE { widget_id, packing_hints, traits, event_callbacks } ) nb =>
MESSAGE { widget_id, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (LABEL { widget_id, packing_hints, traits, event_callbacks } ) nb =>
LABEL { widget_id, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (LIST_BOX { widget_id, scrollbars, packing_hints, traits, event_callbacks } ) nb =>
LIST_BOX { widget_id, scrollbars,
packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks (BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nb
=>
BUTTON { widget_id, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (RADIO_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nb =>
RADIO_BUTTON { widget_id, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (CHECK_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nb =>
CHECK_BUTTON { widget_id, packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks (MENU_BUTTON { widget_id, mitems,
packing_hints, traits, event_callbacks } ) nb =>
MENU_BUTTON { widget_id, mitems,
packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks (TEXT_ENTRY { widget_id, packing_hints, traits, event_callbacks } ) nb =>
TEXT_ENTRY { widget_id, packing_hints,
traits, event_callbacks=>nb };
set_the_widget_event_callbacks (CANVAS { widget_id, scrollbars, citems,
packing_hints, traits, event_callbacks } ) nb =>
CANVAS { widget_id, scrollbars, citems,
packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks (TEXT_WIDGET { widget_id, scrollbars, live_text, packing_hints,
traits, event_callbacks } ) nb =>
TEXT_WIDGET { widget_id, scrollbars, live_text,
packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks (SCALE_WIDGET { widget_id, packing_hints, traits, event_callbacks } ) nb =>
SCALE_WIDGET { widget_id, packing_hints, traits, event_callbacks=>nb };
set_the_widget_event_callbacks pop nb => pop; end;
fun get_the_widget_packing_hints (FRAME { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (MESSAGE { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (LABEL { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (LIST_BOX { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (BUTTON { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (RADIO_BUTTON { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (CHECK_BUTTON { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (MENU_BUTTON { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (TEXT_WIDGET { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (CANVAS { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (POPUP w) => [];
get_the_widget_packing_hints (TEXT_ENTRY { packing_hints, ... } ) => packing_hints;
get_the_widget_packing_hints (SCALE_WIDGET { packing_hints, ... } ) => packing_hints; end;
fun set_the_widget_packing_hints (FRAME { widget_id, subwidgets, packing_hints, traits,
event_callbacks } ) np =>
FRAME { widget_id, subwidgets, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (MESSAGE { widget_id, packing_hints, traits, event_callbacks } ) np =>
MESSAGE { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (LABEL { widget_id, packing_hints, traits, event_callbacks } ) np =>
LABEL { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (LIST_BOX { widget_id, scrollbars, packing_hints, traits, event_callbacks } ) np=>
LIST_BOX { widget_id, scrollbars,
packing_hints=>np, traits, event_callbacks };
set_the_widget_packing_hints (BUTTON { widget_id, packing_hints, traits, event_callbacks } ) np
=>
BUTTON { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (RADIO_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) np =>
RADIO_BUTTON { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (CHECK_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) np =>
CHECK_BUTTON { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (MENU_BUTTON { widget_id, mitems,
packing_hints, traits, event_callbacks } ) np =>
MENU_BUTTON { widget_id, mitems, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (TEXT_ENTRY { widget_id, packing_hints, traits, event_callbacks } ) np =>
TEXT_ENTRY { widget_id, packing_hints=>np,
traits, event_callbacks };
set_the_widget_packing_hints (CANVAS { widget_id, scrollbars, citems,
packing_hints, traits, event_callbacks } ) np =>
CANVAS { widget_id, scrollbars, citems,
packing_hints=>np, traits, event_callbacks };
set_the_widget_packing_hints (TEXT_WIDGET { widget_id, scrollbars, live_text, packing_hints,
traits, event_callbacks } ) np =>
TEXT_WIDGET { widget_id, scrollbars, live_text,
packing_hints=>np, traits, event_callbacks };
set_the_widget_packing_hints (SCALE_WIDGET { widget_id, packing_hints, traits, event_callbacks } ) np =>
SCALE_WIDGET { widget_id, packing_hints=>np, traits, event_callbacks };
set_the_widget_packing_hints pop np => pop; end;
fun get_the_widget_traits (FRAME { traits, ... } ) => traits;
get_the_widget_traits (MESSAGE { traits, ... } ) => traits;
get_the_widget_traits (LABEL { traits, ... } ) => traits;
get_the_widget_traits (LIST_BOX { traits, ... } ) => traits;
get_the_widget_traits (BUTTON { traits, ... } ) => traits;
get_the_widget_traits (RADIO_BUTTON { traits, ... } ) => traits;
get_the_widget_traits (CHECK_BUTTON { traits, ... } ) => traits;
get_the_widget_traits (MENU_BUTTON { traits, ... } ) => traits;
get_the_widget_traits (TEXT_WIDGET { traits, ... } ) => traits;
get_the_widget_traits (CANVAS { traits, ... } ) => traits;
get_the_widget_traits (POPUP { traits, ... } ) => traits;
get_the_widget_traits (TEXT_ENTRY { traits, ... } ) => traits;
get_the_widget_traits (SCALE_WIDGET { traits, ... } ) => traits; end;
fun set_the_widget_traits (FRAME { widget_id, subwidgets, packing_hints, traits, event_callbacks } ) nc
=>
FRAME { widget_id, subwidgets, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (MESSAGE { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
MESSAGE { widget_id, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (LABEL { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
LABEL { widget_id, packing_hints, traits=>nc,
event_callbacks };
set_the_widget_traits (LIST_BOX { widget_id, scrollbars, packing_hints, traits, event_callbacks } )nc
=>
LIST_BOX { widget_id, scrollbars,
packing_hints, traits=>nc, event_callbacks };
set_the_widget_traits (BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
BUTTON { widget_id, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (RADIO_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
RADIO_BUTTON { widget_id, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (CHECK_BUTTON { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
CHECK_BUTTON { widget_id, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (MENU_BUTTON { widget_id, mitems,
packing_hints, traits, event_callbacks } ) nc
=>
MENU_BUTTON { widget_id, mitems,
packing_hints, traits=>nc, event_callbacks };
set_the_widget_traits (TEXT_ENTRY { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
TEXT_ENTRY { widget_id, packing_hints,
traits=>nc, event_callbacks };
set_the_widget_traits (CANVAS { widget_id, scrollbars, citems,
packing_hints, traits, event_callbacks } ) nc
=>
CANVAS { widget_id, scrollbars, citems,
packing_hints, traits=>nc, event_callbacks };
set_the_widget_traits (TEXT_WIDGET { widget_id, scrollbars, live_text,
packing_hints, traits, event_callbacks } ) nc
=>
TEXT_WIDGET { widget_id, scrollbars, live_text,
packing_hints, traits=>nc, event_callbacks };
set_the_widget_traits (SCALE_WIDGET { widget_id, packing_hints, traits, event_callbacks } ) nc
=>
SCALE_WIDGET { widget_id, packing_hints, traits=>nc, event_callbacks };
set_the_widget_traits pop _ => pop; end;
fun get_menu_item_traits (MENU_COMMAND cs) => cs;
get_menu_item_traits (MENU_CHECKBUTTON cs) => cs;
get_menu_item_traits (MENU_RADIOBUTTON cs) => cs;
get_menu_item_traits (MENU_CASCADE(_, cs)) => cs;
get_menu_item_traits _ => []; end;
fun get_the_menu_item_type MENU_SEPARATOR => SEPARATOR_MENU_ITEM_TYPE;
get_the_menu_item_type (MENU_CHECKBUTTON _) => CHECKBOX_MENU_ITEM_TYPE;
get_the_menu_item_type (MENU_RADIOBUTTON _) => RADIO_BUTTON_MENU_ITEM_TYPE;
get_the_menu_item_type (MENU_CASCADE _) => CASCADE_MENU_ITEM_TYPE;
get_the_menu_item_type (MENU_COMMAND _) => COMMAND_MENU_ITEM_TYPE; end;
fun scrolltype_to_horizontal_edge AT_LEFT => LEFT;
scrolltype_to_horizontal_edge AT_RIGHT => RIGHT;
scrolltype_to_horizontal_edge AT_LEFT_AND_TOP => LEFT;
scrolltype_to_horizontal_edge AT_RIGHT_AND_TOP => RIGHT;
scrolltype_to_horizontal_edge AT_LEFT_AND_BOTTOM => LEFT;
scrolltype_to_horizontal_edge AT_RIGHT_AND_BOTTOM => RIGHT;
scrolltype_to_horizontal_edge _ =>
raise exception CONFIG "basic_tk_types::scrolltype_to_horizontal_edge: match exhausted"; end;
fun scrolltype_to_vertical_edge AT_TOP => TOP;
scrolltype_to_vertical_edge AT_BOTTOM => BOTTOM;
scrolltype_to_vertical_edge AT_LEFT_AND_TOP => TOP;
scrolltype_to_vertical_edge AT_RIGHT_AND_TOP => TOP;
scrolltype_to_vertical_edge AT_LEFT_AND_BOTTOM => BOTTOM;
scrolltype_to_vertical_edge AT_RIGHT_AND_BOTTOM => BOTTOM;
scrolltype_to_vertical_edge _ =>
raise exception CONFIG "basic_tk_types::scrolltype_to_vertical_edge: match exhausted"; end;
fun scrolltype_to_opposite_horizontal_edge AT_LEFT => RIGHT;
scrolltype_to_opposite_horizontal_edge AT_RIGHT => LEFT;
scrolltype_to_opposite_horizontal_edge AT_LEFT_AND_TOP => RIGHT;
scrolltype_to_opposite_horizontal_edge AT_RIGHT_AND_TOP => LEFT;
scrolltype_to_opposite_horizontal_edge AT_LEFT_AND_BOTTOM => RIGHT;
scrolltype_to_opposite_horizontal_edge AT_RIGHT_AND_BOTTOM => LEFT;
scrolltype_to_opposite_horizontal_edge _ =>
raise exception CONFIG "basic_tk_types::scrolltype_to_opposite_horizontal_edge: match exhausted"; end;
fun scrolltype_to_opposite_vertical_edge AT_TOP => BOTTOM;
scrolltype_to_opposite_vertical_edge AT_BOTTOM => TOP;
scrolltype_to_opposite_vertical_edge AT_LEFT_AND_TOP => BOTTOM;
scrolltype_to_opposite_vertical_edge AT_RIGHT_AND_TOP => BOTTOM;
scrolltype_to_opposite_vertical_edge AT_LEFT_AND_BOTTOM => TOP;
scrolltype_to_opposite_vertical_edge AT_RIGHT_AND_BOTTOM => TOP;
scrolltype_to_opposite_vertical_edge _ =>
raise exception CONFIG "basic_tk_types::scrolltype_to_opposite_vertical_edge: match exhausted"; end;
fun scrolltype_to_grid_coords scb
=
case scb
AT_LEFT_AND_TOP => ([ROW 1, COLUMN 2], [ROW 2, COLUMN 1], [ROW 2, COLUMN 2]);
AT_RIGHT_AND_TOP => ([ROW 1, COLUMN 1], [ROW 2, COLUMN 2], [ROW 2, COLUMN 1]);
AT_LEFT_AND_BOTTOM => ([ROW 2, COLUMN 2], [ROW 1, COLUMN 1], [ROW 1, COLUMN 2]);
AT_RIGHT_AND_BOTTOM => ([ROW 2, COLUMN 1], [ROW 1, COLUMN 2], [ROW 1, COLUMN 1]); esac;
fun single AT_LEFT => TRUE;
single AT_RIGHT => TRUE;
single AT_TOP => TRUE;
single AT_BOTTOM => TRUE;
single _ => FALSE; end;
fun orient AT_LEFT => TRUE;
orient AT_RIGHT => TRUE;
orient _ => FALSE; end;
};