search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 89 forks source link

combining three-window-mode and delete-empty-windows is bad #124

Open hendriktews opened 8 years ago

hendriktews commented 8 years ago

When I configure three-window-mode and proof-delete-empty-windows Proof General will eventually mess up the window layout. First, I have the script buffer, goals and response. Processing a Lemma, will delete the window with response and when I finish the proof, I just get one with with the response buffer.

Matafou commented 8 years ago

delete-empty-window option should probably be made incompatible with 3 wins mode. If we are in 3 wins mode then we don't want to switch randomly to 2 win mode. We may also remove completely this old option that does make a lot of sense now.

More generally I am not sure what the layout pollicy should be. The users wants: 1) to always see all the outputs of the prover 2) even after having randomly opened and closed frames 3) with a minimal frame moving/popping (If I open a new frame I don't want pg to remove it, or use it to display something else). It is a rather difficult problem.