The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

After investigating more than I wanted, I can summarize what the problem is:

1. the Coq process is associated with the buffers *goals* and *response*
2. the buffers *goals* and *repsonse* are associated with their
respective frames
3. when the Coq process dies, so do the associated buffers.
4. when a buffer dies, so does the associated frame.

Apply transitivity to 3 and 4.

As the source code of proof general notes, there just isn't a good
solution to the above. Well, maybe one could have some sort of a hook
so that when the frames for *goals* and *response* are created, they
could be given attributes that set their size and placement.

The best solution I could come up with was to use C-c r f and C-c r j
to quickly reconstruct the window layouts.

With kind regards,

Andrej