Re: [isabelle] Proper sizing and positioning of windows

Dear Peter,

Sorry for the delay replying to your message. I'm afraid that in the current version of Proof General there isn't an easy way to set positions and sizes of the multiple windows independently. If you are using XEmacs you could try editing proof-multiframe-parameters in generic/pg-response.el to add a default height parameter. (My version of GNU Emacs produces windows of a useful height, they only need a quick rearrangement on the screen which I don't find too troublesome).

I had hoped to support an automatic saving of positions and sizes from session to session but didn't manage to complete the code: Emacs management of windows is a real pain. Patches from users to improve this (or any other) aspect of PG are of course welcome!

Best wishes,

  - David.

On 3 Jan 2006, at 17:36, Peter V. Homeier wrote:

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
(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)
; (list "\\(*isabelle.*-response*\\)" 'height 30 'width 43 'left 748 'top -385) ; (list "\\(*isabelle.*-goals*\\)" 'height 26 'width 126 'left 0 'top 471)
; (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


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?


Peter Homeier
palantir at

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