1

I am using evil (emacs+vim). I am also using Proof General for the theorem prover Coq. I was trying to work with emacs but whenever I do:

:x

or

:q

in my coq .v file all of emacs closes as well (with all my buffers going down). I tried just pressing q on it own but it doesn't work.

I did:

C-x C-c

but that also kills everything and emacs it seems.

I also tried C-x 0 but it says:

Attempt to delete minibuffer or sole ordinary window.

Which doesn't mean much to me. I googled the error and got this Attempt to delete minibuffer or sole ordinary window which didn't clarify things to much.

Does anyone know how I can just close the current coq text file .v without having all of emacs close?


Now I have a new error that after I process part of the Coq script and try to save it and exit, the rest of the panes (buffers? frames?) where the proof context and errors messages are have not been closed...so I end up having to close stuff more times or get stuck...any help?

How do I close a Coq file without it not fully closing and staying within emacs?


To give some more context I am used to using Tmux with Vim + terminal. So doing :x closed my text file and saved it and sent me back to terminal. Thats why I expected it to close my text file but not close emacs (just like it wouldn't close my terminal). I am not saying I necessarily want this behaviour. Perhaps what the issue is that I don't understand what a typical/recommended emacs workflow looks like with ProofGeneral.


Ok, I tried doing what someone suggested which was not to close buffers. Fine. I tried that but now C-x C-f doesn't open files anymore cuz of ProofGeneral :(

  • 1
    Please clarify what you mean by "close". But I think you just want kill-buffer normally bound to C-x k. – Stefan Jan 10 at 3:23
  • @Stefan What I was is to be able to close the buffer and save the file and go back to emacs. If I were in my normal vim+terminal+tmux env I would do :x it would close the file, save it and send me back to my terminal. What puzzles me is why Evil's :x closes ALL of emacs. – Pinocchio Jan 10 at 3:30
  • @Stefan it seems that M-x kill-buffer closed the buffer. But then it sends me to the Proof General welcome screen (and didn't save the file I guess). It's close to what I want but not quite. I would have expected that Evil's vim commands would just work as normal as they do in the terminal. Why don't they work here? – Pinocchio Jan 10 at 3:31
  • I rarely/never "close" buffers: the fact that old buffers "stay within Emacs" just doesn't matter much in practice. – Stefan Jan 10 at 13:44
  • @Stefan I might just be confused on what the typical workflow for emacs usually looks like. I come from Vim+Tmux (not that I necessarily want that work flow) but I think it would be valuable to use ProofGeneral for me when I use Coq. Is the usual workflow to just have lots of buffers open and never close them? I am concerned/confused because ProofGeneral opens additional frames with the proof context etc and when I am done with my current proof script or move to a new one I want to see the frames related to that script not the old one. So I am confused how people work with ProofGeneral. – Pinocchio Jan 11 at 0:11
1

I'm not sure why you expect :x or :wq to save and kill the buffer. From Vim's built-in help:

:[range]x[it][!] [++opt] [file]
            Like ":wq", but write only when changes have been
            made. [...]

:wq [++opt] Write the current file and quit.  Writing fails when
            the file is read-only or the buffer does not have a
            name.  Quitting fails when the last file in the
            argument list has not been edited.

:q[uit] Quit the current window.  Quit Vim if this is the last
        window.  This fails when changes have been made and
        Vim refuses to |abandon| the current buffer, and when
        the last file in the argument list has not been
        edited.

Clearly, :wq saves the buffer, however it either closes the window or quits the program. Apparently you only have one window open which explains why it quits Emacs for you. If you want different behavior, either find a command doing what you want or write your own. :bd is a good candidate here if you want to stick to Ex commands.

  • It's quite natural to expect :x to kill the frame/buffer. To give some more context I am used to using Tmux with Vim + terminal. So doing :x closed my text file and saved it and sent me back to terminal. Thats why I expected it to close my text file but not close emacs (just like it wouldn't close my terminal). I am not saying I necessarily want this behaviour. Perhaps what the issue is that I don't understand what a typical/recommended emacs workflow looks like with ProofGeneral. – Pinocchio Jan 11 at 0:05
  • when it 'sends you back to the terminal', it has closed vim. so when you use the same command in Emacs, I would expect it to close Emacs. If you're running Emacs in a terminal, it won't close your terminal. – Tyler Jan 11 at 0:17
  • Ok, I tried doing what someone suggested which was not to close buffers. Fine. I tried that but now C-x C-f doesn't open files anymore cuz of ProofGeneral :( – Pinocchio Jan 11 at 5:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.