Prevent nesting of sessions, warn on :CoqStart
As an absent-minded person, I often autopilot into typing :CoqStart
when I'm already in a Coq session. When I then go to :CoqQuit
this duplicate session, I find that all the commands have been unset in my initial session and no longer work. It is no longer even possible to :CoqQuit
the outer session to close the extra panes. They have to be closed manually.
I think that :CoqStart
should not be usable once already inside a session. This PR adds a check that the session is not already in progress in the buffer by checking for the coq
buffer variable, which is set in :CoqStart
. If the variable is set, a warning is displayed to the user about preventing nesting, and nothing else happens.