4.7.7 The Preferences structure

maximumHistorySize

Preferences option

Structure

Shell.Options.Preferences

Type

val maximumHistorySize: int option

Description

The maximumHistorySize option is an integer used as the maximum number of history items stored in the listener's History menu. The History menu contains a list of recent declarations previously accepted by the listener. It is 20 by default.

The value of this option appears, and can be set, in the Maximum history length text box on the GUI environment's Preferences > General dialog.

The value of this option has no effect if you are not in the GUI environment.

MLWorks Reference Manual (version 1.0) - 3 DEC 1996

Generated with Harlequin WebMaker