PreviousUpNext

15.4.1239  src/lib/tk/src/basic-tk-types.pkg

## 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;



};



Comments and suggestions to: bugs@mythryl.org

PreviousUpNext