GoToRewriteStep should not be an undoable change

[RazinShaikh]

Moving between rewrite should not be added to the undo stack. This makes actual changes like applying rewrites, renaming proof steps, etc. harder to undo because the user needs to go through all the moving between steps in the undo stack.

[jvdwetering]

What if you do a new rewrite when you are not on the head? Does it then save as a single rewrite step that you've overwritten the current rewrite stack and applied the new rewrite? Although I guess this would overwrite the current undo stack so that might not actually be a problem.

[RazinShaikh]

I don't understand the question. If you do a new rewrite when not at head, then you replace all the subsequent steps with the new rewrite.

[jvdwetering]

And then if you undo, does it remove the last step in the head, and not give back the previous set of rewrite rules? Because then undo does not bring you back to the original state.

[RazinShaikh]

When you undo, it gives back the previous rewrites. That is the current behaviour but I don't think that relies on GoToRewriteStep being undoable

[jvdwetering]

okay, then maybe a different issue: if you go back some steps, and then move some vertices around, moving those vertices should be undoable, but should not remove the current proof stack. However, then the graph diff will look very weird, as that state is still working from the proof head. Or am I misunderstanding how this would work?

[RazinShaikh]

We might need to store at which step the graph is being updated in the undoable command and then automatically switch to that step before performing rest of the undo action

[RazinShaikh]

This is like when you undo in a text editor, your cursor jumps to where the change happened

[jvdwetering]

Ahh, I like that analogy. That makes sense.