Skip to content
  • Isaac van Bakel's avatar
    Prevent nesting of sessions, warn on :CoqStart · 523202b5
    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.
    523202b5