BEGIN
ENABLE
UNWIND => {
IF open THEN stp.Close[ ! STP.Error => TRUSTED {CONTINUE}];
stp ← stp.Destroy
};
expandedName: LONG STRING ← [80];
success: BOOLEAN ← FALSE;
NoteFileProc:
STP.NoteFileProcType =
TRUSTED {
fileInfo: STP.FileInfo ← stp.GetFileInfo[];
continue ← no;
success ← TRUE;
AppendRope[expandedName, file];
bytes ← fileInfo.size;
createDate.length ← 0;
AppendRope[createDate, fileInfo.create];
};
desiredProps: STP.DesiredProperties ← ALL[FALSE];
desiredProps[directory] ← TRUE;
desiredProps[nameBody] ← TRUE;
desiredProps[version] ← TRUE;
desiredProps[createDate] ← TRUE;
desiredProps[size] ← TRUE;
ParseName[fileName, server, rest];
String.AppendChar[expandedName, '[ ];
String.AppendString[expandedName, server];
String.AppendChar[expandedName, '] ];
[] ← stp.Open[Rs[server]];
open ← TRUE;
stp.Login[Rs[name], Rs[password]];
stp.SetDesiredProperties[desiredProps];
stp.Enumerate[Rs[rest], NoteFileProc];
stp.Close[ ! STP.Error => TRUSTED {CONTINUE}];
stp ← stp.Destroy;
IF success THEN {String.Copy[to: fileName, from: expandedName]}
ELSE Error[expl: "File not found", retryable: FALSE];
END;