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
];