Chapter 12

Preferences

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.)

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.