Default preferences are set with the console.addPref function. When you create a preference with console.addPref, a getter/setter pair is automatically created on the console.prefs object. This pair of functions takes care of the actual work of reading from and writing to the user's preference file.
When setting a preference, the value will be converted to be of the same type as the default value for the preference. Preferences are not written to any file until they are actually modified by the user.
Defining and using preferences, from venkman-prefs.js and various files// defining number, boolean, and string preferences console.addPref ("maxStringLength", 100); console.addPref ("enableChromeFilter", true); console.addPref ("lastErrorMode", "ignore"); // reading a pref value if (strval.length > console.prefs["maxStringLength"]) strval = getMsg(MSN_FMT_LONGSTR, strval.length); else strval = strval.quote() // changing a pref value console.prefs["enableChromeFilter"] = e.toggle;
Users can view or change the value of a preference in the Venkman Interactive Session view, by using the /pref command.