Table of Contents
DrJava has many configurable options which can be set using the Preferences command in the Edit menu, allowing the user to change both DrJava's appearance and behavior. Changes made to the configurable options are saved in a
.drjava file in the user's home directory. The Preferences window is the preferred method for setting these options, although more experienced users may also edit the configuration file itself.
The Preferences window is available in the Edit menu, and provides a graphical means to edit all configurable options in DrJava. It displays the options in several categories, each of which can be displayed as a panel of options. Each option has a tool tip with a short description, which can be displayed by holding the mouse arrow over the option.
The Apply button submits the changes on all panels and saves them to the config file, while the OK button does the same and also closes the window. The Cancel button closes the window without applying or saving the changes. Each panel also has a Reset to Defaults button, which resets each of the options on that panel to its original value. Resetting does not take effect until the changes are applied with the Apply or OK buttons.