(*
 * Module Widgets defines the items that are on the UI builder's widgets
 * palette, along with related function and subsidiary objects.  The latter
 * include the properties of the widgets.
 *
 * NOTE: HotKey should probably be promoted up to Widget.
 *
 *)
module Widgets;

  from ToolEnvir import Tool, Canvas, CanvasList, Geometry;
  from IdrawInterface import Selection, SelectionList, GestureMap;
  from Standard import Name;

  op Select(t:Tool, s:Selection)->t':Tool
    post:
	forall (s' in t.cc.sl)
	   IsSelected(s') iff (s = s') and
		(not IsEditable(s)) and (not IsOperable(s));
  end Select;	

  op Run(t:Tool)->(t':Tool)
    post:
	forall (c in t.cl)
	    forall (s in c.sl)
		(exists (c' in t'.cl)
		    (s in c'.sl) and IsOperable(s) and (not IsEditable(s)));
  end Run;

op IsSelected(s:Selection)->boolean;
op IsOperable(s:Selection)->boolean;
op IsEditable(s:Selection)->boolean;

op EditProperties(t:Tool,w:Widget)->(t':Tool,w':Widget)
    post:
	(* Among (many) other things:
	    if w is a menu widget then
	    All hot key assignments for its items unique vis a vis all other
	    hotkeys and the assignments must be set into the
	    hotkeys list of the outputed tool.
         *)
	if (w?<Button) then
	    HotKeysUnique(t', w.<Button) and
                SelectFont(t',w.<Button) and 
	    LabelWidget(t',w.<Button)
	else if (w?<Menu) then
	    HotKeysUnique(t', w.<Menu) and
                SelectFont(t',w.<Menu) and 
	    LabelWidget(t',w.<Menu)
	else if (w?<Text) then
                SelectFont(t',w.<Text) and 
	    Scrollable(t', w.<Text)
	else if (w?<Panel) then
	    Scrollable(t', w.<Panel) and
            if (w?<Radio) then
                SelectFont(t',w.<Radio) and 
		LabelWidget(t',w.<Radio)
            else if (w?<Slider) then
                SelectFont(t',w.<Slider) and 
		LabelWidget(t',w.<Slider)
            else if (w?<FileBox) then
                Scrollable(t',w.<FileBox)
	else
	    true;  (* There should be the remaining cases for the other kinds
		    * of widgets. *)
  end EditProperties;
 
  function HotKeysUnique(t:Tool, w:Widget)->boolean;
    (* Confirm that the hotkey assignments in the given widget are unique within
     * the given tool. *)

  op Sensitize(c:Canvas)->(c':Canvas)
    post:
	forall (s in c.sl)
	    (s in c'.sl) and IsOperable(s) and (not IsEditable(s));
  end Sensitize;

  op Scrollable(t:Tool, w:Widget)->(t':Tool, w':Widget)
    post:
	(* 
	 * If the height of the selections within the canvas' layer is greater
	 * than the height of the canvas layer, or the width of the selections
	 * is greater than the width ofthe canvas layer, then the selections
	 * are scrollable meaning that an appropriately sized (could we use
	 * EqualWidths and EqualHeight from Tool-Env?) scrollbar appears in the
	 * default position, right side for height, and bottom for width.  The
	 * scrollbar may be moved to the opposite location while the
	 * canvas(layer) IsEditable.
	 *)
	if (SumHeights(t.cc.l.sl) > t.cc.l.g.ht) then
	    AddRightScrollbar(t.cc.l)
	else if (SumWidths(t.cc.l.sl) > t.cc.l.g.wd) then
	    AddBottomScrollbar(t.cc.l)
	else	
	    false;		
  end Scrollable;
  
  op AddRightScrollbar(c:Canvas, w:Widget)->(c':Canvas);

  op AddBottomScrollbar(c:Canvas, w:Widget)->(c':Canvas);

  function SumHeights (z:int*) =
 	if ( z = [] ) then
	    0
	else
	    SumHeights (z[1]) + SumHeights (z[2:#z]);

  function SumWidths (z:int*) =
 	if ( z = nil ) then
	    0
	else
	    SumWidths (z[1]) + SumWidths (z[2:#z]);

  obj Widget is g:Graphic and p:Properties and gm:GestureMap;

  obj Widgets is Widget*;

  obj Graphic is SelectionList;

  obj Properties;
  obj ButtonProperties < Properties is Label;
  obj TextProperties < Properties is Label;
  obj LabelProperties < Properties is Label;
  obj MenuProperties < Properties is ... ;
  obj PanelProperties < Properties is ... ;
  obj RadioProperties < Properties is ... ;
  obj SliderProperties < Properties is ... ;
  obj FileBoxProperties < Properties is ... ;
 
  obj Button < Widget is ButtonPalette
    where: Graphic = ButtonGraphic;
	   Properties = ButtonProperties; (* WAS: EditProperties(t:Tool, b:Button).w'.p; *)
  end Button;

  obj ButtonPalette is Layer and ButtonList;

  obj ButtonList is Button*;

  obj ButtonGraphic < Graphic is RoundedRect and Shadow and Label;
	(* Borderline too concrete, but hey, the customer wants it.  And as we
	 * all know, the customer sucks, but he's the boss. *)
  
  op SelectButton(b:Button, bp:ButtonPalette)->(b':Button)
    post:
	forall (b in bp.bl)
	    IsSelected(b');
  end SelectButton;

  op LabelWidget(t:Tool, w:widget) ->(t':Tool);
	(* New widget is given a text string label as its title *)
   	
  op SelectFont(t:Tool, w:widget)->(t':Tool); 
	(* Font selection is made prior to creation of text strings *)

  obj Text < Widget is Layer
    where: Graphic = TextGraphic;
	   Properties = TextProperties;
  end Text;

  obj TextGraphic < Graphic is PortraitRect and Graphic;

  op TextNumberOfLines(tx:Text, lines:integer)->(tx':Text);
  	(* Note: May exceed the height of the Text Widget.
	   User inputs an integer value for number of strings, 
	   with a default value of 1 string that wraps at the 
               TextLineWidth. *)

  op TextLineWidth(tx:Text, lines:integer)->(tx':Text);
	(* Note: 
May exceed the width of the Text Widget *)
  (*
   * Menu widget and its properties.
   *)
  obj Menu < Widget is MenuItemList
    where: Graphic = MenuGraphic;
               Properties = MenuProperties;
  end Menu;
  
  obj MenuItemList is MenuItem*;
  obj MenuItem is Name and HotKey and SubMenu;
  (* Wont work: obj Name is LabelWidget(t:Tool, m:Menu); *)
  obj Name is string;
  obj HotKey is string;
  obj SubMenu is Menu;

  obj Panel < Widget is Layer and Widgets
    where: Graphic = PanelGraphic;
               Properties = PanelProperties;
  end Panel;

  op AlignSelections(p:Panel, sl:SelectionList)->(p':Panel);	

  op ArrangeSelections(p:Panel, sl:SelectionList)->(p':Panel);	

  op GlueSelections(p:Panel, glue:integer)->(p':Panel);

  obj Radio is Layer and ButtonList
    where: Graphic = RadioGraphic;
   	   Properties = RadioProperties;
  end Radio;

  op SelectMark(r:Radio, mark:SelectionList)->(r':Radio);

  obj Slider is SliderPalette
    where: Graphic = SliderGraphic;
	   Properties = SliderProperties;
  end Slider;

  obj SliderPalettes is Layer and SliderList;

  obj SliderList is Slider*;

  op GetValues(s:Slider, beginval:integer, endval:integer, step:integer)->
	(s':Slider);

  obj FileBox is Layer 
    where: Graphic = FileBoxGraphic;
	   Properties = FileBoxProperties;
  end FileBox;
	
  op SelectItemList(fb:FileBox, sl:SelectionList)->(fb':FileBox);

end Widgets;