1. package Widgets.Menu_Items.Menu_Checkboxes is 
  2.  
  3.     -- Extends Menu_Item, implementing a toggle-able menu item. Menu checkboxes 
  4.     -- display a checkbox to the left of their label and toggle their state 
  5.     -- when clicked. 'Selected' actions will fire when the checkbox becomes 
  6.     -- checked, and 'Unselected' actions will fire when the checkbox becomes 
  7.     -- unchecked. 
  8.     type Menu_Checkbox is new Menu_Item with private; 
  9.     type A_Menu_Checkbox is access all Menu_Checkbox'Class; 
  10.  
  11.     -- Creates a new menu checkbox widget within 'view' with id 'id'. 'text' is 
  12.     -- the item's display text. 'checked' is the initial state of the checkbox. 
  13.     function Create_Menu_Checkbox( view    : not null access Game_Views.Game_View'Class; 
  14.                                    id      : String; 
  15.                                    text    : String := ""; 
  16.                                    checked : Boolean := False 
  17.                                  ) return A_Menu_Checkbox; 
  18.     pragma Precondition( id'Length > 0 ); 
  19.     pragma Postcondition( Create_Menu_Checkbox'Result /= null ); 
  20.  
  21. private 
  22.  
  23.     type Menu_Checkbox is new Menu_Item with 
  24.         record 
  25.             checked : Boolean := False;    -- stated of the checkbox 
  26.         end record; 
  27.  
  28.     procedure Construct( this    : access Menu_Checkbox; 
  29.                          view    : not null access Game_Views.Game_View'Class; 
  30.                          id      : String; 
  31.                          text    : String; 
  32.                          checked : Boolean ); 
  33.     pragma Precondition( id'Length > 0 ); 
  34.  
  35.     procedure Draw_Content( this : access Menu_Checkbox; dc : Drawing_Context ); 
  36.  
  37.     procedure Handle_Mouse_Release( this : access Menu_Checkbox; 
  38.                                     evt  : not null A_Mouse_Button_Event ); 
  39.  
  40. end Widgets.Menu_Items.Menu_Checkboxes;