17c17
<  * in the calendar tool system.
---
>  * in the calendar system.
25,27c25,27
<   from Admin import UserId, AdminPassword, AdminEmailAddress;
<   from Options import RegularUserOptions, AdministrativeOptions;
<   export FileSpace, File, FileSize;
---
>   from Admin import UserId;
>   from Options import Options;
>   export FileSpace, File;
40c40
<         file_type:FileType and data:FileData and size:FileSize;
---
>         file_type:FileType and data:FileData;
79,81c79,81
<         The type of file data is either CalendarType data (which we care
<         about), SettingsType data (which we also care about), or any other
<         type of data (which we don't care about).
---
>         The type of file data is either CalendarType data (which we care about)
>         or any other type of data that can be stored in a file, which we don't
>         care about.
107,113d106
<   object FileSize is integer
<     description: (*
<        Size in bytes of the file.
<     *);
<   end FileSize;
< 
< 
131,132c124
<          * 2-last+1 in the output workspace.  The number of unnamed calendars
<          * is incremented by one.
---
>          * 2-last+1 in the output workspace.
140,142c132,134
<             (#(uws'.calendars) = #(uws.calendars) + 1) and
<             (forall (i:integer | (i &gt;= 1) and (i &lt;= #(uws.calendars)))
<                 uws'.calendars[i+1] = uws.calendars[i]
---
>             (#(uws'.calendars) = #(uws.calendars) +1) and
>             (forall (i:integer | (i &gt;= 2) and (i &lt;= #(uws.calendars)))
>                 uws'.calendars[i+1] = uws.calendars[i+1]
193c185
<     inputs: uws:UserWorkSpace;
---
>     inputs: fs:FileSpace, uws:UserWorkSpace;
263,270d254
<   object AdminSettingsFile is
<     components: passwd:AdminPassword and email:AdminEmailAddress and
<         options:AdministrativeOptions;
<     description: (*
< 
<     *);
<   end AdminSettingsFile;
<