-
Notifications
You must be signed in to change notification settings - Fork 86
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Buffer coq-compile-response sometimes takes over the whole window #54
Comments
I have just also seen this happen in sequential background compilation mode. |
This happens every time the pg windows are messed up. I don't really
understand when this happens. Sometimes the goals window takes the whole
frame, sometimes its the compilation window.
Workaround: type "M-x dedicated-mode" twice.
If someone understand why windows do mess sometimes, we can fix this maybe.
|
maybe related to #42? |
Do you still see the reported behavior? Can you give some more hints for reproducing? @Matafou What do you mean with the "pg windows are messed up" ? |
I did not do very much work with Coq recently, so I can't really tell... I don't actively remember seeing this recently, but I also don't think that means much. Sorry :/ |
I just saw this happen again, using (slightly outdated) PG 60dcd96 |
What PG configuration do you use, especially how many windows? Is coq-compile-response usually in a separate window? The issue descriptions sounds like some dedicated-window property is getting in the way. When it happens the next time, can you try evaluating
via eval-expression? |
Here's my
If "window" here means "X11 window", then the answer this that all the three buffers are in the same window, the left left of which is taken over by the |
So it just happened again and I did the |
OK, this seems to confirm that the dedicated flag is the problem. How about using C-x 0 (which invokes delete-window) or C-x 1 (delete-other-windows)? This works at least for me when three-window-mode messes up. |
... I meant to use C-x 0 and C-x 1 until you have one emacs window left and then use C-x b to switch to you coq code and then use C-x 1? |
Yeah, "C-x 0 C-C C-l" works to fix the mess. (Btw, currently, the issue seems to be 100% reproducible.) |
Ralf Jung notifications@github.com writes:
Would you mind telling how to reproduce? |
I am now getting the following Coq error displayed in the window where the
The layout is "messed up", I cannot switch buffers in this window, etc. |
This makes #54 a bit less critical.
Just to confirm, after doing the final C-c C-Ret the emacs frame BTW, the proper PG way to fix broken window layouts is I just pushed a partial fix that makes this issue a bit less A proper solution is a bit more involved. We first have to decide
Then of course it should disappear again at the right time. |
I do.
I know; however, that binding is not available when the coq-compile-response buffer is active.
So this means I can just C-c C-b back to the buffer that I was in previously? That would indeed help a lot.
I would think it should appear where Coq output always appears, in the bottom right quarter. I actually wasn't even aware that this is not the same buffer. |
Ralf Jung notifications@github.com writes:
But it is bound in Goals and response, you could do C-x o first, right? You can also always do M-x proof-layout-windows.
Yes.
I agree. The problem is to ensure the response buffer will show up in the same window when there is some response from the toplevel later on. There are good reasons to have two different buffers. One shows response from the toplevel and the other shows standard output from coqc or coqdep. The latter one is in compilation-mode to enable the next-error feature. |
I guess I could. Any reason it is not bound in coq-compile-response?
I see. What is that next-error feature? If PG is able to automatically jump to where the background compilation error occurred, then I wasn't aware of that. |
Ralf Jung notifications@github.com writes:
Good point - no there is no reason.
Yes, it's C-x `. There is not always a line number, but if there |
Remove install targets for other provers
Sometimes when there is an error while compiling files (parallel compilation in background enabled), the buffer
*coq-compile-response*
pops up to cover the entire window (as in, the X11 window) of emacs. In this case, switching back to the buffer that I am actually editing is impossible; emacs says I cannot switch buffers in a "dedicated window". I have to kill multiple buffers to go on working; usually I just restart emacs.Unfortunately, I found no way to reproduce this.
The text was updated successfully, but these errors were encountered: