int GetNumber(DviWidget);