Anubis / Anubis

   
   
                             The Anubis/Paradize Project.
   
                                  The button widget. 
   
                        Copyright (c) Alain Prouté 2004-2005. 

   
   Authors:   Alain Prouté
              Olivier Duvernois


   
read tools/basis.anubis   
read widget.anubis
read tools.anubis
   
   
   In this  file the 'button' widget  is defined.  The role  of a button is  to perform an
   action when it  is clicked upon. Actually,  this action is not performed  when the left
   button  of the  mouse is  pushed down,  but only  when it  is released,  and  under the
   condition that the mouse cursor is still within the button. That way the user still has
   the possibility to renounce to the action.
      
   Buttons also change their aspect not only when left clicked on, but also when the mouse
   cursor rolls over them. This is an important ergonomic feature, because the user better
   understands the possible consequences of the  action of the button.  This may also help
   to detect the presence of the button, which may sometimes not be so obvious.
   
   Furthermore, a button may  reflect a state.  For example, a button  may be a flip-flop,
   and change the  state of some variable at each  click. In this case, it  is a good idea
   that the  button has differents decorations  depending on the state.   For that reason,
   the decoration of the button is  not constant, but recomputed when needed.  Also, since
   these decorations may not have the same size, the size of the button does not depend on
   them. This is also preferable for making tables of buttons. That way we may ensure that
   the size of the buttons do not depend on their current decoration.
   
   Since a  button may  reflect a  'state', the button  must eventually  monitor a  set of
   variables, so that its decoration is always  up to date.  The following tool enables to
   monitor such a variable without having to create a monitor.
   
public type ButtonRegistration:...       // an opaque type   
   
public define ButtonRegistration
   register
     (
       Var($T) variable
     ). 
   
   For example, if the  state (hence the decoration) of your button  depends on the values
   of the variables 'v1', 'v2' and 'v3'  (whose types may be different), use the following
   list as the last argument of 'create_button':
   
        [
          register(v1),
          register(v2),
          register(v3)
        ]
   
   That way you ensure that if the value of any of these variables changes, the decoration
   of your button changes accordingly at the (almost) same time.
   
   Summarizing, a button has 3 aspects:
   
     - normal:         the mouse cursor is outside the area of the button
     - rolled over:    the mouse cursor is within the area of the button but not left 
                         clicked
     - clicked:        the mouse cursor is within the area of the button and left clicked
   
   and its  decoration (reflecting a state) may  change.  Of course its  action in general
   depends on this state.
   
   We propose the following styles of presentation for buttons:
   
public type ButtonStyle:
   nude,                                         // nothing except the current decoration
   push_down (WidgetParameters parameters),      // standard 'push down' aspect
   phantom   (WidgetParameters parameters).      // has a relief only when rolled over
   
   Typically, 'nude'  buttons are used for  making hypertext links,  'phantom' buttons are
   used for making menu items.

   We also  allow the  following sorts of  decorations. Decorations are  always vertically
   centered, but  may be either  left justified or  horizontally centered. In the  case of
   image and text together, the image is placed on the left of the text. 
   
public type ButtonDecoration:
   center_text             (WidgetParameters,String), 
   left_text               (WidgetParameters,String), 
   center_image            (HostImage),
   left_image              (HostImage),
   center_image_and_text   (WidgetParameters,HostImage,String),
   left_image_and_text     (WidgetParameters,HostImage,String). 
   
   
   A button is created by:
   
public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> One         action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       One -> Bool                 is_inhibited, 
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ). 

public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> 
         List(WidgetRectangle)           action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       One -> Bool                 is_inhibited, 
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ). 

public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> One         action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ). 

public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> 
         List(WidgetRectangle)           action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ). 


   
   
   --- That's all for the public part ! --------------------------------------------------
   

   
   --------------------------- Table of Contents -----------------------------------------
   
   
   ---------------------------------------------------------------------------------------
   
   
   
   Above we  have discussed a notion  of state for a  button. This notion  arises from the
   fact  that  the button's  action  and  decoration may  depend  on  the  values of  some
   variables. This will be called the 'major state' of the button. 
   
   Now, the button has another sort of state, the 'minor state', described by:
   
type MinorState:   
   up,                  // the mouse cursor is not on the button
   rolled_over,         // the mouse cursor is on the button, which is still up
   down.                // the button is down (has been left clicked)
   
      
   
   
   
   *** (1) Drawing the button. 
   
   Drawing the  button depends on the  style of the  button (nude, push down,...)   on the
   nature of the decoration (text, image,...) and  on its minor state.  We have a function
   for drawing the decoration, and an auxiliary functions for each style of button.
   
   
define One
   draw_text
     (
       WidgetDrawToolBox   dtb, 
       String              t,
       SystemFont          font, 
       Bool                inhibited, 
       WidgetParameters    parms, 
       Int32               button_width, 
       Int32               button_height,
       Int32               font_height, 
       Int32               x,
       Int32               th,
       WidgetRectangle     clip
     ) =
   with y = (Int32)(font_height+((button_height-th)/2)), 
   forget(draw(dtb)(t,
                    font,
                    if inhibited
                      then *dark_color_v(parms)
                      else *font_color_v(parms),
                    position(x,y), 
                    clip));
   if inhibited
   then forget(draw(dtb)(t,
                    font,
                    if inhibited
                      then *light_color_v(parms)
                      else *font_color_v(parms),
                    position(x+1,y+1), 
                    clip))
   else unique. 
   
   
   
   
define One
   draw_decoration
     (
       WidgetDrawToolBox              dtb,    
       ButtonDecoration        decoration,
       Bool                     inhibited, 
       Int32                 button_width,
       Int32                button_height,
       Int32                  left_margin,     // used by 'left_...' decorations
                                               // and also between image and text
       WidgetRectangle               clip      // clipping rectangle for decoration
     ) =
   if decoration is 
     {
       center_text(parms,t) then 
         with      font = *font_v(parms), 
                   info = get_font_info(font),
            font_height = word8_to_int32(height(info)), 
                     th = font_height+word8_to_int32(depth(info)), 
                     tw = printed_text_width(font,t), 
         draw_text(dtb,t,font,inhibited,parms,button_width,button_height,font_height,
                   (button_width-tw)/2,th,clip),   
           
       left_text(parms,t) then 
         with      font = *font_v(parms), 
                   info = get_font_info(font),
            font_height = word8_to_int32(height(info)), 
                     th = font_height+word8_to_int32(depth(info)), 
                     tw = printed_text_width(font,t), 
         draw_text(dtb,t,font,inhibited,parms,button_width,button_height,font_height,
                   left_margin,th,clip),
   
       center_image(i) then 
         if size(i) is (iw,ih) then
         draw(dtb)(i,
                   position((button_width-iw)/2,
                            (button_height-ih)/2),
                   clip), 
   
       left_image(i) then 
         if size(i) is (iw,ih) then
         draw(dtb)(i,
                   position(left_margin,
                            (button_height-ih)/2),
                   clip), 
   
       center_image_and_text(parms,i,t) then 
         if size(i) is (iw,ih) then
         with      font = *font_v(parms), 
                   info = get_font_info(font),
            font_height = word8_to_int32(height(info)), 
                     th = font_height+word8_to_int32(depth(info)), 
                     tw = printed_text_width(font,t), 
                    itw = iw+left_margin+tw,
         draw(dtb)(i,
                   position((button_width-itw)/2,
                            (button_height-ih)/2),
                   clip);
            draw_text(dtb,t,font,inhibited,parms,button_width,button_height,font_height,
                   ((button_width-itw)/2)+left_margin+iw,th,clip),

       left_image_and_text(parms,i,t) then 
         if size(i) is (iw,ih) then
         with      font = *font_v(parms), 
                   info = get_font_info(font),
            font_height = word8_to_int32(height(info)), 
                     th = font_height+word8_to_int32(depth(info)), 
                     tw = printed_text_width(font,t), 
                    itw = iw+left_margin+tw,
         draw(dtb)(i,
                   position(left_margin,
                            (button_height-ih)/2),
                   clip);
            draw_text(dtb,t,font,inhibited,parms,button_width,button_height,font_height,
                      left_margin+iw+left_margin,th,clip),              
     }.
   
   
   
define One
   draw_nude_button
     (
       WidgetDrawToolBox          dtb, 
       Int32                    width,          // width of button
       Int32                   height,          // height of button
       ButtonDecoration    decoration,
       Bool                 inhibited
     ) =
   draw_decoration(dtb,decoration,inhibited,width,height,0,rect(0,0,width,height)). 
   
   
define One   
   draw_push_down_button  
     (
       WidgetDrawToolBox          dtb,
       Int32                    width,   // of button
       Int32                   height,
       RGB                 main_color,
       RGB                light_color,
       RGB                 dark_color,
       MinorState              mstate,
       ButtonDecoration    decoration,
       Bool                 inhibited
     ) =
   draw(dtb)(rect(2,2,width-2,height-2),main_color);
   with black = rgb(0,0,0), 
     draw_relief_edge(dtb,1,rect(0,0,width,height),black,black); 
   if mstate is 
     {
       up then 
         draw_relief_edge(dtb,1,rect(1,1,width-1,height-1),light_color,dark_color),
   
       rolled_over then 
         //draw(dtb)(rect(1,1,width-1,height-1),light_color); 
         draw_relief_edge(dtb,1,rect(1,1,width-1,height-1),light_color,dark_color),
   
       down then 
         draw_relief_edge(dtb,1,rect(1,1,width-1,height-1),dark_color,dark_color)
     };
   draw_decoration(dtb,decoration,inhibited,width,height,3,rect(3,3,width-3,height-3)). 
   
   
define One   
   draw_phantom_button    
     (
       WidgetDrawToolBox         dtb,
       Int32                   width,
       Int32                  height,
       RGB                main_color,
       RGB               light_color,
       RGB                dark_color,
       MinorState             mstate,
       ButtonDecoration   decoration,
       Bool                inhibited
     ) =
   draw(dtb)(rect(0,0,width,height),main_color); 
   if mstate is 
     {
       up then 
         unique, 
   
       rolled_over then 
         draw_relief_edge(dtb,1,rect(0,0,width,height),light_color,dark_color),
   
       down then 
         draw_hollow_edge(dtb,1,rect(0,0,width,height),light_color,dark_color),   
     };
   draw_decoration(dtb,decoration,inhibited,width,height,3,rect(3,3,width-3,height-3)). 
   
   
   
   
define One
   draw_button
     (
       Int32                        width, 
       Int32                       height, 
       ButtonStyle                  style, 
       WidgetDrawToolBox              dtb,
       MinorState                  mstate,
       ButtonDecoration        decoration,
       Bool                     inhibited
     ) =
   if style is 
     {
       nude then 
         draw_nude_button(dtb,width,height,decoration,inhibited), 
   
       push_down(parms) then 
         if parms is parameters(main_color_v,
                                light_color_v,
                                dark_color_v,
                                _,_,_,_,_,_,_,_) then 
         draw_push_down_button(dtb,
                               width,height,
                               *main_color_v,*light_color_v,*dark_color_v,
                               mstate,
                               decoration,inhibited),
   
       phantom(parms) then 
         if parms is parameters(main_color_v,
                                light_color_v,
                                dark_color_v,
                                _,_,_,_,_,_,_,_) then 
         draw_phantom_button(dtb,
                             width,height,
                             *main_color_v,*light_color_v,*dark_color_v,
                             mstate,
                             decoration,inhibited)
     }. 
   
   
   

   
   
   *** (3) The captured mouse handler. 
   
   We uncapture the mouse as soon as the mouse pointer is outside the button. This amounts
   to recapture the mouse with a 'fake' mouse handler doing just nothing.
   
define WidgetAnswer
   fake_mouse_handler
     (
       KeyboardState                 ks,
       WidgetMouseCapturedEvent       e
     ) =
   not_handled([]). 
   
   Now, here  is the  function which  constructs the actual  captured mouse  handler. This
   handler just detects  if the mouse cursor is  outside the button. As soon as  it is the
   case, the button  is redrawn and the  mouse is uncaptured (i.e. recaptured  by the fake
   mouse handler).
   
define WidgetEventToolBox -> ((KeyboardState ks, WidgetMouseCapturedEvent e) -> WidgetAnswer)
   make_captured_mouse_handler
     (
       Int32                               width, 
       Int32                              height, 
       Var(MinorState)                mstate_loc,
       WidgetEventToolBox -> 
         List(WidgetRectangle)            action
     ) =
   (WidgetEventToolBox etb) |->
   (KeyboardState ks, WidgetMouseCapturedEvent e) |->
     with xe = x(e), ye = y(e), 
       if (0 =< xe & xe < width & 0 =< ye & ye < height)
       then if e is 
         {
           moved(x,y)       then handled([]),
           liberated(x,y)   then (mstate_loc <- rolled_over; 
                                  with rects = action(etb),
                                  handled([rect(0,0,width,height) . rects]))
         }
       else mstate_loc <- up; 
            forget(capture_mouse(etb,fake_mouse_handler));
            handled([rect(0,0,width,height)]). 
     
      
   
   
   
   *** (4) Handling normal events. 
   
   
   The button must  detect if it received a  left down or left up button  click. Note that
   the event received is  always within thearea of the button. We  assigns the right value
   to the minor state variable, and eventually execute the action.
   
   
             event_handler(etb,e,width,height,mstate_loc,action), 
   
 read widgets3/trace.anubis
   
define WidgetAnswer
   event_handler
     (
       WidgetEventToolBox                     etb, 
       WidgetNormalEvent                        e,
       Int32                                width, 
       Int32                               height,
       Var(MinorState)                 mstate_loc,
       WidgetEventToolBox -> 
         List(WidgetRectangle)             action,
       (KeyboardState, 
        WidgetMouseCapturedEvent) 
          -> WidgetAnswer               cmhandler,
       One -> Bool                   is_inhibited
     ) =
   if is_inhibited(unique) then handled([]) else
   if e is 
     {
       mouse_gone then 
         if *mstate_loc is 
           {
             up           then handled([]), 
             rolled_over  then mstate_loc <- up; handled([rect(0,0,width,height)]),
             down         then mstate_loc <- up; handled([rect(0,0,width,height)])
           },
   
       mouse_move(ks,x,y) then 
         if *mstate_loc is 
           {
             up           then mstate_loc <- rolled_over; handled([rect(0,0,width,height)]),
             rolled_over  then handled([]), 
             down         then handled([])
           },
   
       mouse_click(ks,mc,x,y) then 
         if *mstate_loc is 
           {
             up           then if mc is left_down 
                               then (mstate_loc <- down; 
                                     forget(capture_mouse(etb,cmhandler)); 
                                     handled([rect(0,0,width,height)]))
                               else handled([]),
   
             rolled_over  then if mc is left_down 
                               then (mstate_loc <- down; 
                                     forget(capture_mouse(etb,cmhandler)); 
                                     handled([rect(0,0,width,height)]))
                               else handled([]),
   
             down         then if mc is left_up 
                               then (with rects = action(etb),
                                     mstate_loc <- up;
                                     handled([rect(0,0,width,height) . rects]))
                               else handled([])
           }
     }.

   
   
   *** (5) Modifying registrations. 
   
   When  the button  is created,  the  user creates  a list  of 'ButtonRegistration',  not
   depending  on the  type of  the  variables to  be monitored.   The function  'register'
   declared in  the public part  of this file,  must encapsulate the variable  within some
   tool (i.e. function)  able to produce a 'WidgetRegistration'  from that variable. Hence
   the definition of type 'ButtonRegistration':
   
public type ButtonRegistration:
   button_registration(((WidgetMonitoringToolBox mtb, 
                         List(WidgetRectangle) -> One redraw) -> One) -> WidgetRegistration).
   
   
   New, 'register' is defined using 'register' defined in 'widget.anubis'. 
   
public define ButtonRegistration
   register
     (
       Var($T) variable
     ) =
   button_registration(
       ((WidgetMonitoringToolBox, List(WidgetRectangle) -> One) -> One m) |-> 
          register(variable,m)). 
   
   
   When  the   monitor  'm'   is  available,   each  function  (tool)   in  the   list  of
   'ButtonRegistration' is mapped to it, producing the final list of 'WidgetRegistration'.
   This mapping is acheived by:
   
define List(WidgetRegistration)
   transform
     (
       List(ButtonRegistration)                                        bregs,
       (WidgetMonitoringToolBox,List(WidgetRectangle) -> One) -> One   m
     ) =
   if bregs is 
     {
       [ ] then [ ], 
       [breg1 . others] then if breg1 is button_registration(tool) then 
         [tool(m) . transform(others,m)]
     }.
   
   
   

   *** (6) Creating the button. 
   
   
public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> 
         List(WidgetRectangle)           action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // decoration of the button
       One -> Bool                 is_inhibited,      // inhibition test
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ) =
   with mstate_loc = var((MinorState)up), 
           monitor = (WidgetMonitoringToolBox mtb, List(WidgetRectangle) -> One redraw) |-> 
             redraw([rect(0,0,width,height)]), 
         cmhandler = make_captured_mouse_handler(width,height,mstate_loc,action), 
   create_widget
     (
       /* Setting positions of childs */ 
       (WidgetPositionToolBox ptb) |-> unique, 
   
       /* Getting size */ 
       (One u) |-> (width,height), 
   
       /* Redrawing */ 
       (WidgetDrawToolBox dtb) |-> 
          draw_button(width,height,style,dtb,*mstate_loc,get_decoration(unique),is_inhibited(unique)), 
 
       /* duplicate */   
       (One u) |-> create_button(width,height,style,action,get_decoration,is_inhibited,registrations), 

       /* Change size */ 
       (Int32 w, Int32 h) |-> unique, 
   
       /* Handling normal events */ 
       (WidgetEventToolBox etb, WidgetNormalEvent e) |->
          event_handler(etb,e,width,height,mstate_loc,action,cmhandler(etb),is_inhibited), 
   
       /* Registrations */ 
       transform(registrations,monitor)
     ).


   
   
public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> One         action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       One -> Bool                 is_inhibited, 
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ) =
   create_button(width,
                 height,
                 style,
                 (WidgetEventToolBox etb) |-> (action(etb); []),
                 get_decoration, 
                 is_inhibited,
                 registrations). 
   
public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> One         action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ) =
   create_button(width,
                 height,
                 style,
                 (WidgetEventToolBox etb) |-> (action(etb); []),
                 get_decoration, 
                 (One u) |-> false,
                 registrations). 
   

public define Widget
   create_button
     (
       Int32                              width,      // total width of button in pixels
       Int32                             height,      // total height of button in pixels
       ButtonStyle                        style,      // style of drawing for the button
       WidgetEventToolBox -> 
         List(WidgetRectangle)           action,      // action performed by the button
       One -> ButtonDecoration   get_decoration,      // getting the decoration of the button
       List(ButtonRegistration)   registrations       // list of variables monitored by the button
     ) =
   create_button(width,
                 height,
                 style,
                 action,
                 get_decoration, 
                 (One u) |-> false,
                 registrations).