(****
 *
 * Module RolodexTool defines the top-level tool object that contains the
 * currently active rolodex and system state information.  Also in the module
 * are File and Edit objects that define abstractions for the file space and
 * clipboard to be supplied by the underlying operating environment.
 *
 *)
module RolodexTool;

  from Rolodex import Rolodex;
  from File import FileSpace, File;
  from Edit import ClipBoard;

  export WorkSpace, SystemState, Banner;

  object RolodexTool is FileSpace and ClipBoard and Rolodex and SystemState;

  object RolodexOperation is op()->();
 
  object WorkSpace is rolodex:Rolodex and current_file:File and
        state:SystemState;

  object SystemState is requires_saving:boolean and unsaved_empty:boolean;

  object Banner is string;

  operation InvokeFromOS is
    inputs: ;
    outputs: RolodexTool;
    precondition: ;
    postcondition: ;
    description: (*
        
    *);
  end InvokeFromOS;

  operation PerformOperation
    inputs: rt:RolodexTool, ro:RolodexOperation;
    outputs: rt':RolodexTool;
    precondition: IsPerformable(ro, rt);
    postcondition: CorrectStateTransition(rt, rt', ro);
    description: (*
	    
    *);
  end PerformOperation;

  function IsPerformable(RolodexOperation, RolodexTool) -> boolean;

  function CorrectStateTransition(rt:RolodexTool, rt':RolodexTool,
        ro:RolodexOperation) = (

    (if ChangesRolodex(ro) then
	CorrectRolodexStateTransition(rt, rt', ro))

	and

    (if ChangesFileSpace(ro) then
	CorrectFileSpaceStateTransition(rt, rt', ro))

	and

    (if ChangesEditSpace(ro) then
	CorrectEditSpaceStateTransition(rt, rt', ro));

  );

  func ChangesRolodex(ro:RolodexOperation) -> boolean = ( ... );
  func CorrectRolodexStateTransition(rt:RolodexTool, rt':RolodexTool,
        ro:RolodexOperation) -> boolean = ( ... );
  func ChangesFileSpace(ro:RolodexOperation) -> boolean = ( ... );
  func CorrectFileSpaceStateTransition(rt:RolodexTool, rt':RolodexTool,
        ro:RolodexOperation) -> boolean = ( ... );
  func ChangesEditSpace(ro:RolodexOperation) -> boolean = ( ... );
  func CorrectEditSpaceStateTransition(rt:RolodexTool, rt':RolodexTool,
        ro:RolodexOperation) -> boolean = ( ... );

end RolodexTool;