(****
 *
 * Module View defines the objects and operations related to the different
 * calendar views available to the user.  The structural viewing levels are
 * item, day, week, month, and year.  There are operations to go to the
 * previous and next views at any level, as well as an operation to go to a
 * specific date.  Lists of scheduled items can be viewed in a variety of ways.
 * A general view filter operation can be applied to both structural and list
 * views.  Operations are available to view other users' calendars and to view
 * a list of active viewing windows.
 *
 * NOTE: this is work in progress.  A good deal of objects are yet to be
 * defined.
 *
 *)
module View;

  import CalendarDB.CalendarDB, CalendarDB.UserCalendar,
         CalendarDB.UserWorkSpace, CalendarDB.CalendarName;
  import Schedule.ScheduledItem, Schedule.StartTime, Schedule.Duration,
         Schedule.Title, Schedule.Category, Schedule.Location,
         Schedule.Security, Schedule.Priority, Schedule.Date, Schedule.Hours,
         Schedule.Minutes, Schedule.DateNumber, Schedule.Time, Schedule.Hour,
         Schedule.Minute, Schedule.AmOrPm, Schedule.DayName,
         Schedule.MonthName;
  export CustomLists, Filtering, WindowingMode;

  object DailyAgenda
    components: Date and EventTitle* and TimeSlotDescriptor* and
        TaskDescriptor*;
    description: (*
        A DailyAgenda contains scheduled item information for a calendar day.
        The Date indicates the day of the agenda.  The EventTitle list contains
        the titles of zero or more events scheduled to occur on this day.  The
        TimeSlotDescriptor list contains time-tagged descriptors for scheduled
        appointments and meetings.  The TaskDescriptor list is a numbered list
        of tasks scheduled to be due on this day.
    *);
  end DailyAgenda;

  object EventTitle = Title
    description: (*
        The title of an event as shown in the list of events for a day.
    *);
  end;

  object TimeSlotDescriptor
    components: TimeSlotName and BriefItemDescriptor* and Overlaps;
    description: (*
        A time slot descriptor represents one slot (physically, a row) in a
        daily agenda.  The TimeSlotName component is the start time for the
        slot.  The list of BriefItemDescriptors contains the items that begin
        within the slot, where "within" is defined as the start time plus the
        current time increment.  The overlaps component is a list of items with
        start times that overlap with an item in the BriefItemDescriptor list.
    *);
  end TimeSlotDescriptor;

  object TimeSlotName = Time
    description: (*
        A TimeSlotName consists of a numeric TimeValue and an AmOrPm indicator.
    *);
  end TimeSlotName;

  object BriefItemDescriptor
    components: Title and StartTime and Duration and Category;
    description: (*
        A brief item descriptor contains a subset of the information for a full
        scheduled item.  The information is a Title, StartTime, Duration, and
        Category.
    *);
  end BriefItemDescriptor;

  object Overlaps
    components: BriefItemDescriptor*;
    description: (*
        Overlaps contain zero or more BriefItemDescriptors that overlap with
        with the master item in a given time slot.  An overlapping item is one
        with a StartTime within the same time slot as other items.  The
        "master" item in a time slot is the item that is first in a sorted
        order based on start time, duration, and alphabetic title as the
        primary, secondary, and tertiary sort keys, respectively.
    *);
  end Overlaps;

  object TaskDescriptor
    components: TaskNumber and TaskTitle;
    description: (*
        A TaskDescriptor is one item in a number list of tasks.
    *);
  end TaskDescriptor;

  object TaskNumber = integer
    description: (*
        The ordinal number of a task relative to other tasks.
    *);
  end;

  object TaskTitle = Title
    description: (*
        The free-form title of a task.
    *);
  end;

  object DailyFormatOptions
    components: NormalTimeRangeOption and TimeIncrementOption and
        IncrementHeightOption and ShowHide24HoursOption and
        ShowHideExactTimeOption and ShowHideDashedLinesOption and
        ShowHideExtensionArrowsOption and ProportionalSpacingOnOffOption and
        DisplayOverlapsOption and ShowHideEventsOption and
        ShowHideTasksOption and DefaultHeightAndWidthOption;
    description: (*
        DailyFormatOptions control the details of how daily agenda information
        is formated.
    *);
  end DailyFormatOptions;

  object NormalTimeRangeOption = StartTime and EndTime
    description: (*
        NormalTimeRangeOption defines the starting and ending times that
        normally appear in the left column of the daily agenda.  The default
        range of times is 8AM to 5PM.
    *);
  end;

  object TimeIncrementOption = Hours and Minutes
    description: (*
        TimeIncrementOption defines the time increment of the left column
        labels in the daily agenda.  The smallest allowable time increment is
        five minutes, the largest is twelve hours.  When the time increment is
        less than one hour, the time labels are shown in hour and minute
        format; when the increment is one hour or greater, the labels are shown
        as hours with no minutes.  The default increment is one hour.
    *);
  end;

  object IncrementHeightOption = integer
    description: (*
        IncrementHeightOption option defines the default minimum number of text
        lines shown in each time increment of a daily agenda.  If there are
        more items starting in an increment than fit in the minimum number of
        lines, the system automatically increases the height for that increment
        to a size sufficient to display all items fully.  The default value is
        two lines per increment.
    *);
  end;

  object ShowHide24HoursOption is Show or Hide
    description: (*
        ShowHide24HoursOption toggles between showing a full 24 hours of
        display versus the normal time range only in daily agenda.  If the
        24-hour time range is shown, non-normal times are shown with a light
        grey background, to distinguish them from normal times.  The default
        value for this option is to hide non-normal times.
    *);
  end;

  object ShowHideExactTimeOption = Show or Hide
    description: (*
        ShowHideExactTimeOption toggles between showing or not showing the
        starting and ending times for each scheduled item immediately to the
        left of the title in a daily agenda.  This option is useful when items
        do not typically start or end exactly on the hour.  The default value
        for this option is to hide the exact time.
    *);
  end;

  object ShowHideDashedLinesOption = Show or Hide
    description: (*
        ShowHideDashedLinesOption toggles between showing and not showing the
        dashed lines that appear above and below items that do not start or end
        on the hour in a daily agenda.  The default is to show dashed lines.
    *);
  end;

  object ShowHideExtensionArrowsOption = Show or Hide
    description: (*
        ShowHideExtensionArrowsOption toggles between showing and not showing
        the down-pointing arrows for items with end times that extend beyond
        the hour of the start time in a daily agenda.  The default is to show
        extension arrows.
    *);
  end;

  object ProportionalSpacingOnOffOption = On or Off
    description: (*
        ProportionalSpacingOnOffOption toggles between placing items
        proportionally down from the top of the hour based on starting time in
        a daily agenda.  When the option is off, the first (only) item in an
        hour is placed at the top of that hour and any other items starting in
        the hour are placed immediately below it.  The default is proportional
        spacing on.
    *);
  end;

  object DisplayOverlapsOption = Horizontal or Vertical
    description: (*
        DisplayOverlapsOption controls how items with overlapping times are
        displayed in a daily agenda.  When displayed horizontally, overlapping
        items appear side-by-side in separate columns of the day view.  When
        displayed vertically, overlapping items appear on separate lines in a
        single column, sorted by start time, duration, and title.  The default
        is horizontal display.
    *);
  end;

  object ShowHideEventsOption = Show or Hide
    description: (*
        ShowHideEventsOption toggles between showing or not showing the list of
        events in a daily agenda.  The default is to show events if any are
        scheduled.
    *);
  end;

  object ShowHideTasksOption = Show or Hide
    description: (*
        ShowHideTasksOption toggles between showing or not showing the list of
        tasks in a daily agenda.  The default is to show tasks if any are
        scheduled.
    *);
  end;

  object DefaultHeightAndWidthOption = Height and Width
    description: (*
        DefaultHeightAndWidthOption controls the width and height of the full
        daily agenda.  If one or both of the default dimensions is too small to
        accommodate all information in the display, the information is
        truncated appropriately and scrollbars are added to the display window.
    *);
  end;

  object EndTime = TimeSlotName
    description: (*
        Ending time in the normal time range option.
    *);
  end;

  object Show
    description: (*
        Option indicator for a show/hide option, indicating that the option
        state is "show".
    *);
  end;

  object Hide
    description: (*
        Option indicator for a show/hide option, indicating that the option
        state is "hide".
    *);
  end;

  object On
    description: (*
        Option indicator for an on/off option, indicating that the option state
        is "on".
    *);
  end;

  object Off
    description: (*
        Option indicator for an on/off option, indicating that the option state
        is "off".
    *);
  end;

  object Horizontal
    description: (*
        Option indicator for displaying overlaps horizontally.
    *);
  end;

  object Vertical
    description: (*
        Option indicator for displaying overlaps vertically.
    *);
  end;

  object Height = integer
    description: (*
        Height value for the default height and width option.
    *);
  end;

  object Width = integer
    description: (*
        Width value for the default height and width option.
    *);
  end;

  object WeeklyAgendaTable
    components: ;
    description: (*
        
    *);
  end WeeklyAgendaTable;

  object WeeklyAgendaList
    components: ;
    description: (*
        
    *);
  end WeeklyAgendaList;

  object MonthlyAgenda
    components: FullMonthName and FirstDay and NumberOfDays and SmallDayView*;
    description: (*
        A MonthlyAgenda contains a full month name, the day of the week for its
        first day, and the number of days.  Scheduled item data are contained
        in a small daily view for each day of the month, organized in a fashion
        typical in paper calendars.
    *);
  end MonthlyAgenda;

  object FullMonthName
    components: MonthName and YearNumber;
    description: (*
        The full name of a month, consisting of the month name and the year.
    *);
  end FullMonthName;

  object YearNumber = integer
    description: (*
        The year number, between 0 and 9999.
    *);
  end YearNumber;

  object FirstDay = DayName
    description: (*
        The name of the first day of a month, i.e., the day the month starts
        on.
    *);
  end FirstDay;

  object NumberOfDays = integer
    description: (*
        The number of days in a month, between 28 and 31.
    *);
  end NumberOfDays;

  object SmallDayView
    components: DateNumber and BriefItemDescriptor*;
    description: (*
        A SmallDayView has the number of the date and a list of zero or more
        brief item descriptors.
    *);
  end SmallDayView;

  object YearlyCalendar = YearNumber and SmallMonthView*
    description: (*
        A YearlyCalendar contains a year number and a small view for each
        month, organized in four 3-month rows.
    *);
  end YearlyCalendar;

  object SmallMonthView
    components: MonthName and FirstDay and NumberOfDays and DateNumber*;
    description: (*
        A SmallMonthView is an abbreviated version of a monthly agenda, with a
        MonthName instead of a FullMonthName, and a collection of DateNumbers
        instead of SmallDayViews.
    *);
  end SmallMonthView;

  operation ViewItem(CalendarDB)->ScheduledItem;

  operation ViewDay(cdb:CalendarDB)->agenda:DailyAgenda
    postcondition:
        (*
         * The output agenda is for the currently selected date, if any,
         * today's date otherwise.
         *)
        ;
    description: (*
        ViewDay produces a DailyAgenda for the currently selected date in the
        given calendar DB, or for today's date if no other date is currently
        selected.
    *);
  end ViewDay;

  operation ViewWeekTable(CalendarDB)->WeeklyAgendaTable;
  operation ViewWeekList(CalendarDB)->WeeklyAgendaList;
  operation ViewMonth(CalendarDB)->MonthlyAgenda
    description: (*
        The output is taken both from the user's own calendar as well as the
        system version of the user's calendar when the latter contains
        penciled-in meetings.
    *);
  end;
        
  operation ViewYear(CalendarDB)->YearlyCalendar;

  operation GotoNext(CalendarDB)->ViewLevel;
  operation GotoPrevious(CalendarDB)->ViewLevel;
  operation GotoDate(CalendarDB)->ViewLevel;

  operation ViewAppointmentsList(CalendarDB)->AppointmentsList;
  operation ViewMeetingsList(CalendarDB)->MeetingsList;
  operation ViewTasksList(CalendarDB)->TasksList;
  operation ViewEventsList(CalendarDB)->EventsList;
  operation ViewAllItemsList(CalendarDB)->AllItemsList;

  operation ViewOtherUser(CalendarDB)->UserCalendar;

  operation ViewWindows(CalendarDB)->WindowNameList;

  operation ViewCalendars(CalendarDB)->CalendarNameList;

  object ViewLevel = ScheduledItem or DailyAgenda or WeeklyAgendaTable or
        WeeklyAgendaList or MonthlyAgenda or YearlyCalendar;

  object AppointmentsList = AppointmentListItem*
    description: (*
        An AppointmentsList is the collection of items that appear in the list
        view of appointments.
    *);
  end;

  object MeetingsList = MeetingsListItem*
    description: (*
        A MettingsList is the collection of items that appear in the list
        view of meetings.
    *);
  end;

  object TasksList = TasksListItem*
    description: (*
        A TasksList is the collection of items that appear in the list
        view of tasks.
    *);
  end;

  object EventsList = EventsListItem*
    description: (*
        An EventsList is the collection of items that appear in the list
        view of events.
    *);
  end;

  object AllItemsList = ListItem*
    description: (*
        An AllItemsList is the collection of items that appear in the list
        view of all scheduled items.
    *);
  end;

  object AppointmentListItem
    components: Title and Date and Time and Duration and Recurs and
        Category and Location and Security and Priority;
    description: (*
        An AppointmentListItem is the somewhat abbreviated description of an
        appointment that appears in appointments and meetings list views.  The
        precise relation between a full Appointment compared to an
        AppointmentListItem is as follows:
								       <ul><li>
	    The titles are the same.
									   <li>
	    The list item has only a start date, with no end date.  This is
	    because there is a separte list item for every instance of a
	    recurring appointment.
									   <li>
	    The start time and duration are the same.
									   <li>
            There is only a boolean-valued Recurs component in the list item,
	    instead of the full recurring structure of the Appointment.  The
	    rationale is that the list would be too cluttered if it contained
	    all of the recurring information of the full appointment.
									   <li>
	    The category, location, security, and priority are the same.
									   <li>
	    The list item contains no remind information or details.  The
	    rationale is again not to clutter the list.
								          </ul>
    *);
  end AppointmentListItem;

  (* TBD: *)
  obj MeetingsListItem;
  obj TasksListItem;
  obj EventsListItem;
  obj ListItem;

  object Recurs = boolean
    description: (*
        Indicates in an AppointmentsListItem whether the appointment recurs.
    *);
  end Recurs;

  object WindowNameList = WindowName*;
  object WindowName = string;

  operation SelectDate(cdb:CalendarDB, date:Date)->(cdb':CalendarDB)

    postcondition:
        (*
         * The selected date in the current calendar is set to the given date.
         *)
        cdb'.workspace.calendars[1].selected_date = date;

    description: (*
        Select a date in the current calendar.  The most typical reason for
        date selection is as the argument to a view command.
    *);

    end SelectDate;

  (*
   * A major bit of aux function spec will be opaque functions that define the
   * externally defined day/date computations.
   *)


  (* TBD: *)
  object CustomLists;
  object Filtering;

  object WindowingMode = TwoWindow or PerLevel or MultiWindow
    description: (*
        The WindowingMode is one three levels, which indicate how many display
        windows can be visible at any given time.
    *);
  end;

  object TwoWindow
    description: (*
        The windowing mode in which at most two windows are displayed -- one
        window for all calendar views and another window for all list views.
    *);
  end;

  object PerLevel
    description: (*
        The windowing mode in which one window is displayed for each level of
        calendar display, item through year, and one window is displayed for
        each type of list.  In this mode, up to eleven windows are displayed at
        one time, five for the calendar views (item, day, week, month, year)
        and six for the list views (appointments, meetings, events, all items,
        custom lists).
    *);
  end;

  object MultiWindow
    description: (*
        The windowing mode in which the results of each and every view command
        are displayed in a separate window.  In this mode, an indefinite number
        of windows can be displayed at any one time.  Multi-window mode is most
        typically used for createing side-by-side displays of consecutive
        calendar views, such as a three-week display.
    *);
  end;

  object CalendarNameList
    components: CalendarName;
    description: (*
       The list of names of all open calendars.  Non-unique names are suffixed
       with a unique integer.
    *);
  end CalendarNameList;

end View;