three windows mode at pg start when a warning window

[courtieu]

To reproduce it:

set the three-pane mode to true by setting the emacs variable proof-three-window-enable to t.

be sure to have a warning message at pg start (for example by using a different version of emacs thant the one it was compiled for).

open a .v file

Effect: the .v file is not displayed, the warning buffer + the response buffer are displayed instead.

[courtieu]

One more comment: It is impossible to configure pg to *really* start in 3 pane mode anyway. You still need to hit C-c C-l. This is probably linked.

Best regards, P.

[David Aspinall]

Hi Pierre,

I guess you mean 3-window mode with the two-column layout you prefer? The other layout is horizontal splitting, which is the default until the user triggers re-layout with C-c C-l. This was by design to allow users to move windows around themselves, but I guess we could easily add a call to layout windows at start of scripting.

[David Aspinall]

Actually, I suppose you're thinking that it would be nice to start PG immediately showing 3 windows? Unfortunately that's a bit tricky because the buffers are generated dynamically when the proof shell is fired up. We would need a new option and function to layout windows in this eager fashion.

I still haven't repeated the warning message thing (probably a different problem, issue with splash screen).

[David Aspinall]

I've added an option to eagerly layout windows but it has some problems, partly because your code for three window layout (proof-select-three-b) uses interactive functions that switch buffers in ways that depend on which buffers are selected at the time, but we don't want to change selected buffers during startup. So I've had to change that. This also clashes with the splash screen which attempts to save the window layout. It is all pretty messy and I doubt we're going to have a perfectly intuitive display of buffers etc (whatever that might mean).

Some fixes are still needed at the moment because now the three window mode goes wrong and leaves two displays of the response buffer for some reason.

[courtieu]

Replying to da:

Actually, I suppose you're thinking that it would be nice to start PG immediately showing 3 windows?

No I don't want the resp and goals buffer to appear immediately. I want them to appear when scripting starts only.

Unfortunately that's a bit tricky because the buffers are generated dynamically when the proof shell is fired up. We would need a new option and function to layout windows in this eager fashion.

No no we do not want that. People often open coq files to simply read them.

I still haven't repeated the warning message thing (probably a different problem, issue with splash screen).

What I should do first is to remove everything concerning three windows mode from coq.el and see what happens...

[courtieu]

Replying to da:

I've added an option to eagerly layout windows but it has some problems, partly because your code for three window layout (proof-select-three-b) uses interactive functions that switch buffers in ways that depend on which buffers are selected at the time, but we don't want to change selected buffers during startup. So I've had to change that. This also clashes with the splash screen which attempts to save the window layout. It is all pretty messy and I doubt we're going to have a perfectly intuitive display of buffers etc (whatever that might mean).

I just committed a nil by default for this option, but anyway we should simply remove.

*BUT* the bug with response buffer hiding script buffer is still there if three-window enabled.

[courtieu]

I don't understand the response buffer bug. Maybe it is related to the

but putting proof-layout-window in

proof-activate-scripting-hook fixes it. However this forces the horizontal splitting because proof-layout-window forces it (when three-win on).

I think proof-layout-windows should conform to an option proof-horizontal-splitting-policy-for-three-window-mode (or anything shorter :)).

This variable should have the following meaning:

nil : no horizontal splitting 'smart : follow the `display-buffer' policy (if frame is large enough then split horizontally otherwise stay in vertical splitting) that would be the default setting. 't : always split horizontally

Notice that when three-window is disabled, the 'smart policy is the one followed by proof-layout-window.

What do you think? P.

[courtieu]

Replying to courtieu:

I don't understand the response buffer bug. Maybe it is related to the

Sorry for the unfinished sentence. It may be related to the change in proof-get-window-for-buffer I made some time ago but I don't see why. Investigating.

[courtieu]

Replying to courtieu:

I don't understand the response buffer bug. Maybe it is related to the

but putting proof-layout-window in

proof-activate-scripting-hook fixes it. However this forces the horizontal splitting because proof-layout-window forces it (when three-win on).

I think proof-layout-windows should conform to an option proof-horizontal-splitting-policy-for-three-window-mode (or anything shorter :)).

This variable should have the following meaning:

nil : no horizontal splitting 'smart : follow the `display-buffer' policy (if frame is large enough then split horizontally otherwise stay in vertical splitting) that would be the default setting. 't : always split horizontally

I implemented and committed it in cvs.

Variable name is proof-three-window-mode-policy The values are 'vertical 'horizontal or 'smart. I think it is nice like that.

[courtieu]

Marked as fixed:

• The three windows are not displayed before scripting really starts.
• proof-laytout-windows is called when scripting really starts (this fixes the bug where resp buffer was hiding scriopt buffer).
• proof-laytout-windows is now cleaner: it always refresh windows layout (even in 2 win mode) and it adapts to the current width of the frame (both in 2 and 3 win modes).