-
Isaac van Bakel authored
As an absent-minded person, I often autopilot into typing `:CoqStart` when I'm already in a Coq session. This results in a nested session appears inside the narrow code pane, and which is itself made up of even narrower panes. When I then go to `:CoqQuit` this duplicate session and get back my normally-proportioned Coq session, I find that all the commands have been unset and no longer work. In fact, it is no longer even possible to `:CoqQuit` the outer session to close the extra panes. They have to be closed manually. This all points to a simple conclusion: nesting sessions makes no sense, and `:CoqStart` should not be usable once already inside a session. This commit 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. Since the variable is unset in `:CoqQuit`, it is possible to start, quit, and restart sessions as usual.