feat: adding alt + shift click to expand all ellipsis goals #871
Conversation
| const {mode, depth, coqCss, id, indent, breaks, boxChildren, hovered, maxDepth, addedDepth} = props; | ||
| const [hide, setHide] = useState<boolean>(depth >= maxDepth); | ||
| const {mode, depth, coqCss, id, indent, breaks, boxChildren, parentHide, hovered, maxDepth, addedDepth} = props; | ||
| const [selfHide, setSelfHide] = useState<HideStates>(ComputeHideState(depth >= maxDepth ? HideStates.HIDE : HideStates.UNHIDE, parentHide)); | ||
| const [depthOpen, setDepthOpen] = useState<number>(addedDepth); |
There was a problem hiding this comment.
One thing I might add, I was a bit confused about the depthOpen variables usage, so maybe there is a simpler solution to the "expand all the way" problem using that variable?
There was a problem hiding this comment.
depthOpen controls at what depth an ellipsis will open. So when you click on an ellipsis, instead of only unfolding it's child, it will go down depthOpen which is more comfortable than having to unfold one by one.
There was a problem hiding this comment.
Sorry to clarity, depthOpen tracks the current depth at which an ellipsis happens, so the depth until which eveything is open. The ADDED_DEPTH_FACTOR just allows us to increment this in steps larger than 1.
|
I wonder, should it not be a button "Unfold all"? This way it's more accessible to newcomers? |
|
We could add an unfold all button, but I believe it would be different. In this case it just unfolds one ellipsis all the way to the bottom. Unfold all would open everything right ? |
rtetley
changed the title
|
Thanks for your contribution ! Just took the liberty of documenting the shortcuts. Concerning the Open all button we can move that to a separate issue ! |
Given the following case where you have a goal that is collapsed:
You can use
alt + clickto expand it to something like this:However, I frequently find myself wanting to expand all the way if I am doing expanding, so I added a feature such that
alt + shift + clickwill expand the original to this instead (note that no ellipsis remain as it will expand everything below the clicked on ellipsis):Additionally, I found some typos while adding this feature and fixing them is included as well.