7. Customizing the Display

There are two ways of customizing the frame display when using Isamode: by setting Emacs user-options and by setting X resources.

7.1 Display options

The user options controlling the display mostly appear in the file `isa-display.el'.

User Option: isa-multiple-frame-mode

If non-nil, use multiple frames.
Setting this to nil restricts Isabelle-interaction mode to use a single frame.

To toggle this setting while Isamode is running, use the function isa-toggle-multi-frame.

The default value is nil.

Command: isa-toggle-multi-frame &optional set

Toggle use of multiple frames, or switch on if arg non-nil.

User Option: isa-startup-defaults

List of symbol names of associated buffers to initialise by default.
The buffers on this list will be automatically started when an Isabelle session is started.

The default value starts a proofstate display and a ruletable display.

The list of symbols allowed is given by isa-possible-associated-buffer-names.

The default value is (proofstate).

Variable: isa-possible-associated-buffer-names

Names of types of buffers which may be associated to an Isabelle session.

Variable: isa-default-menubar

The base menubar (in XEmacs format) for Isabelle interaction mode.
A value of nil means the only menus that appear are the Isabelle ones. You can set this to default-menubar (in XEmacs), to have the usual menus in addition. This may clutter the display a little, or result in menus being lost off the end of the menubar!

7.2 Display options, continued

Variable: isa-single-frame-display-props

Display properties for Isabelle buffers in single frame mode.
This variable controls the default heights for the various Isabelle buffers in single frame mode, and also a ``shrink to fit'' attribute. It is an association list of mode symbols and cons cells, of the form:

     (mode-name    (prop-list))

where prop-list is a list of property cons values, of the form

     (window-height . integer)  or  (shrink-to-fit . boolean)

(Note: these properties are implemented inside Isamode and are not a standard part of XEmacs.)

The default value for isa-single-frame-display-props is:

(setq isa-single-frame-display-props       
   ((proofstate-mode     (window-height . 8)) 
    (listener-mode       (window-height . 5))
    (ruletable-mode      (window-height . 15))
    (ruletable-mode      (shrink-to-fit . t)))
)

Variable: isa-multi-frame-display-props

Display properties for Isabelle buffers in multiple frame mode.
This variable controls the the default frame parameters for multiple frame mode. It is an association list used to set symbol properties. The properties are standard XEmacs ones.

The default value for isa-multi-frame-display-props looks something like this:

(setq isa-multi-frame-display-props      
  '((proofstate-mode     (frame-name . proofstate))
    (listener-mode       (frame-name . listener))
    (ruletable-mode      (frame-name . ruletable))
    (isa-mode            (frame-name . isabelle))
    (ruletable           (instance-limit . 3))
    (ruletable           (max-frame-height . 25))
    (ruletable           (frame-defaults .
                           ((top . 560)   (left . 5)
                            (height . 22) (width . 60)
                            (menu-bar-lines . 0)
                            (minibuffer . nil)                          
                            )))
    (isabelle            (frame-defaults .             
                          ((top .  0)    (left .  0)        
                           (height . 35) (width . 80)   
                           )))
    (listener            (frame-defaults .
                          ((top . 620)   (left . 530)
                           (height . 7)  (width . 65)
                           (menu-bar-lines . 0)
                           (minibuffer . nil)
                           )))
    (proofstate          (frame-defaults .
                          ((top .  30)    (left . 700)
                           (height . 35)  (width . 50)
                           (menu-bar-lines . 0)
                           (minibuffer . nil)
                           (vertical-scroll-bars . nil)
                           ))))
)

This shows the setting of the frame names for the Isabelle buffer modes (which automatically gives them individual X-windows), and the frame default parameters for each of the frame names. Some of these values may be inappropriate for your display, so you may wish to change them in your `~/.emacs'.

See See Info file `(lispref)', node `Frame Parameters' for more information about frame parameters.

7.3 X Resources

Frame properties are an unsatisfactory part of the Emacs window interface: the kind of settings they control are usually kept in the X resources database. Luckily, XEmacs allows X resources to be used in place of isa-multi-frame-display-props.

Here are some sample X defaults for XEmacs that work well on my X terminal. See the file `etc/Xdefaults-xemacs' in the Isamode distribution for more examples, and the documentation in See Info file `emacs', node `Resources X'. Further details are in See Info file `elisp', node `X Frame Parameters'.

/*  ===== X resources for Isamode in XEmacs ===== */

/* some frame geometries. */

Emacs*listener.geometry:   55x10
Emacs*ruletable.geometry:  57x15
Emacs*proofstate.geometry: 52x35

/* ruletable frames have large red headings */

Emacs*ruletable.ruletableGroupname.attributeFont:  \
        -adobe-helvetica-bold-r-normal--*-160-75-75-*-*-iso8859-1

Emacs*ruletable.ruletableGroupname.attributeForeground: red

/* proofstate frames have bold goal subgoal numbers */
 
Emacs*proofstate.proofstateGoal.attributeFont:  \
        -adobe-courier-bold-r-normal--*-140-75-75-*-*-iso8859-1
Emacs*proofstate.proofstateSubgoalNumber.attributeFont:  \
        -adobe-courier-bold-r-normal--*-140-75-75-*-*-iso8859-1

Frame properties take precedence over X resources, so you will need

   (setq isa-multi-frame-display-props 
    '((proofstate-mode     (frame-name . proofstate))
      (listener-mode       (frame-name . listener))
      (ruletable-mode      (frame-name . ruletable))
      (isa-mode            (frame-name . isabelle))
      (ruletable           (instance-limit . 3))))

or something similar in your `~/.emacs' to ensure the resource specifications have effect.

Go to the first, previous, next, last section, table of contents.