[isabelle] Proper sizing and positioning of windows



I have just upgraded to Isabelle2005 from the 2002 version.  One feature that I 
liked was that I could set the sizes and positions of the three windows (frames)
used for the script buffer, goals buffer and response buffer, by setting the value
of the Emacs variable `special-display-regexps' in the file /usr/local/Isabelle/etc/proofgeneral-settings.el,
by something like the following script:

; Separate windows for response and goal buffers (suggestion from David Oheimb)
(setq special-display-regexps (append (list
;1024x768:
(list "\\(*isabelle.*-response*\\)" 'height 19 'width 60  'left 585 'top 0  )
(list "\\(*isabelle.*-goals*\\)"    'height 22 'width 60  'left 585 'top 340)
; (list "\\(*isabelle.*-response*\\)" 'height 35 'width 52  'left 677 'top -247)
; (list "\\(*isabelle.*-goals*\\)"    'height 20 'width 134 'left 0   'top  450)
;1152x900:
; (list "\\(*isabelle.*-response*\\)" 'height 30 'width 43  'left 748 'top -385)
; (list "\\(*isabelle.*-goals*\\)"    'height 26 'width 126 'left 0   'top  471)
;1400x1280:
; (list "\\(*isabelle.*-response*\\)" 'height 30 'width 90  'left 661 'top  494)
; (list "\\(*isabelle.*-goals*\\)"    'height 30 'width 90  'left 661 'top -545)
; to push the response/goals windows to the right margin, use:
;(list "\\(*isabelle.*-response*\\)" 'height 30 'width 90  'left 740 'top 494)
;(list "\\(*isabelle.*-goals*\\)"    'height 30 'width 90  'left 740 'top -545)
) special-display-regexps))

(note: most of the lines are commented out by the initial semicolon; they are retained as different versions for different screens.)

This worked fine in Isabelle2002, and produced the three frames in the predetermined positions on each launch of Isabelle under ProofGeneral.

However in Isabelle2005, this seems to be ignored.  Is there some new way to specify this behavior?  I have read the documentation page

file:///usr/local/ProofGeneral/doc/ProofGeneral/ProofGeneral_7.html

about the display options available, including proof-three-window-enable and proof-multiple-frames-enable.
Turning these on does generate the three desired frames, but the goals and response
buffer windows are small (~10 lines), not the sizes or positions I would like.  
This seems unaffected by the modification to the special-display-regexps as above.

Rather than adjust them by hand for every launch of Isabelle, is there a way to 
set these default locations/positions, as there used to be?

Thanks!

Peter Homeier
palantir at trustworthytools.com





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.