MenuPrivate:
TYPE =
RECORD [
choices: ChoiceS,
header: Image,
doc: ROPE,
allMayBeUp: BOOL,
left, top: Label,
fullRows, arrayRows, cols, timeOut: NAT,
height, width: NAT -- total size of menu, in pixels -- ¬ 0,
rowHeight, colWidth: NAT ¬ 0,
leftLabelSize, topLabelSize, headerSize, fullRowHeight, fullRowsSize: NAT ¬ 0,
arrayLeft, arrayRight, arrayBot, arrayTop, arrayHeight, arrayWidth: NAT ¬ 0,
headerBot, fullRowsBot: NAT ¬ 0
];