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

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


ProofGeneral-devel mailing list

Reply via email to