This PR updates the dock key bindings according to the following model:
There are three bits:
Visible: Opened / closed.
Focus: Panel focused / center focused.
Zoom: Zoomed / Not zoomed.
Each of these variables is 'sticky' in that they won't effect each other
unless they need to. 'Zooming' a panel conceptually merges the visible
and focus bits.
cmd-shift-j/b/r have all been removed.
cmd-j/b/r have been updated to mean 'toggle visibility of a certain
dock', firing them should *always* reveal the panel to you (where you
last left it), or hide it, without moving focus (unless the focused
element is invisible). This means that, when the terminal panel is
zoomed, cmd-j has the same effect as ctrl-`
ctrl-` and cmd-shift-e now toggle a panel's focus, without updating the
zoom state of a panel. Toggling the focus of a zoomed panel causes it to
automatically hide itself, without losing the zoom bit.
When focused or made visible, panels which cannot be zoomed
automatically unzoom everything else so as to preserve user intent of
'show me this panel' and 'everything stays where it is if I don't take
an action'
Release Notes:
- cmd-shift-j/b/r have been removed. (preview only)
- cmd-j/b/r unconditionally show or hide their associated dock,
respecting zoom settings. (preview only)
- ctrl-` and cmd-shift-e now retain zoom state. (preview only)
- Fixed a bug where terminal dock tab would always be in the active
state (preview only)
- Fixed a bug where terminals would not always open in the terminal
panel
- Changed the look of zoomed panels to fill more of the screen (preview
only)
584e5f7958