MrEd supports a number of preferences for global configuration. The
MrEd preferences are stored in the common file reported by
find-system-path for 'pref-file (see
Pathnames, section 11.3.1 in PLT MzScheme: Language Manual), and preference values can be
retrieved and changed through get-preference and
set-preference as defined by MzLib's file library
(see file.ss, chapter 18 in PLT MzLib: Libraries Manual). However, MrEd
reads most preferences once at startup (all except the
'|MrEd:playcmd| preference).
The following are the preference names used by MrEd. (The preference names are case-sensitive, hence the quoting vertical bars around each symbol.)
'|MrEd:default-font-size| preference -- sets the default font size
the basic style in a style list, and thus the default font size for
an editor.
'|MrEd:wheelStep| preference -- sets the default mouse-wheel step
size of editor-canvas% objects.
'|MrEd:outlineInactiveSelection| preference -- a true, non-zero
value causes selections in text editors to be shown with an outline
of the selected region when the editor does no have the keyboard
focus.
'|MrEd:playcmd| preference -- used to format a sound-playing
command; see play-sound for details.
'|MrEd:forceFocus| preference -- a true, non-zero value enables
extra effort in MrEd to move the focus to a top-level window that is
shown or raised.
'|MrEd:doubleClickTime| preference -- overrides the
platform-specific default interval (in milliseconds) for double-click
events.
'|MrEd:gamma| preference -- sets the gamma value used in
gamma-correcting PNG files.
In addition, preference names built from font face names can provide
or override default entries for the font-name-directory<%>;
see Font Preferences for information.