Hi, my last commit fixes the problem that Proof General was screwing up the displayed buffers when switching the active scripting buffer with Coq. Let me explain:
I use the 2-windows mode of Proof General, usually one frame showing the current scripting buffer and either *goals* or *response*. Let's say a.v is the active scripting buffer, but I want to do something in b.v. So I switch buffer to b.v and start scripting there. Before my last commit, the result was that Proof General was finally showing an empty *response* buffer. This was very annoying. Proof General was doing the following: - retract a.v completely, thereby changing the window configuration to show b.v and *response* - kill coqtop, thereby killing *response* and as a result the window configuration changes to show b.v and a.v. For some strange reason b.v is the least recently selected window now. - start coq for the new scripting buffer and start sending the initialization commands - after the first init command, Proof General decides it should show *response*, and finally calls (proof-get-window-for-buffer "*response*"). There, the first if selects the else branch and the next if calls (display-buffer "*response*"). Because b.v is least recently selected, the window configuration changes to show *response* and a.v. - For some reason a.v disappeared during processing other init commands. I thought about a heuristic that avoids to replace the current scripting buffer in proof-get-window-for-buffer. However, I finally decided to kill the *response* window before killing the *response* buffer. Please check that this change does not have some unwanted side effects. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
