This is a patch for a possible window management feature. The current functionality has it so that both C-c C-g (lean-toggle-show-goal) and C-c C-n (lean-toggle-next-error) create their own windows. However, there can be a lot of overlap in information between them, so I find myself toggling windows frequently. This, unfortunately, messes up my window layout because of the behavior of display-buffer. While this can be fixed somewhat with a user-defined display-buffer-alist, I thought it would be nicer to have these buffers share a window.
This commit changes lean-toggle-info-buffer to look for a window containing an info buffer, and reuse it if one exists. But, if one exists and it is for the requested type of buffer, then that window is closed, implementing the toggling functionality. Also, if the user has manually created a second window so that both the goals and errors are visible, then each toggling command will close its respective window.
Kha
commented
4 years ago
This is a patch for a possible window management feature. The current functionality has it so that both
C-c C-g(lean-toggle-show-goal) andC-c C-n(lean-toggle-next-error) create their own windows. However, there can be a lot of overlap in information between them, so I find myself toggling windows frequently. This, unfortunately, messes up my window layout because of the behavior ofdisplay-buffer. While this can be fixed somewhat with a user-defineddisplay-buffer-alist, I thought it would be nicer to have these buffers share a window.This commit changes
lean-toggle-info-bufferto look for a window containing an info buffer, and reuse it if one exists. But, if one exists and it is for the requested type of buffer, then that window is closed, implementing the toggling functionality. Also, if the user has manually created a second window so that both the goals and errors are visible, then each toggling command will close its respective window.