homotopy-rs
homotopy-rs copied to clipboard
homotopy-io
"Undo" beahaviour
I think any changes to what one is currently viewing (i.e. which slice/depth) shouldn't count as actions, for the purposes of the "undo" command. At the moment it's a bit frustrating trying to find out how many times I need to click "undo" to undo the last actually meaningful action performed. When I change slice/depth to try to check if I got back to the state I want, I end up adding more actions to the stack and I get stuck in a swamp.
I've often been frustrated by the way undo works. I think this is a very good suggestion.
I see that this is fixed now, which is great! What would be even better would be if Undo and Redo didn't change the current view, so I could see what is happening from the view that I have selected.
I am reopening this because I had to revert the change due to an unforeseen problem. I will re-implement it as well as your other suggestion about undo/redo not changing the view as part of a proposed refactoring of proof state (#837).
I have abandoned the proposal in #837 and I think we need to store the view state in the history for things to work correctly.
However, there are other ways we could achieve this. We could for example make it so that when you undo, it skips over all the non-meaningful actions like SwitchSlice. So we will still store these actions in the history, thereby ensuring the action dump is deterministic, but we allow undo to undo more than one action at a time.
I see that this is fixed now, which is great! What would be even better would be if Undo and Redo didn't change the current view, so I could see what is happening from the view that I have selected.
This is however impossible (or at least too difficult to get right).
I feel like it should be possible in limited circumstances (e.g. if the workspace diagram didn't change, then undo/redo could preserve the current view)
But that's already the case...
What Manuel wanted is that if you have done a contraction and are looking inside a slice, pressing undo should undo the contraction while leaving you inside that slice (or the corresponding slice in the diagram before the contraction).