Allow case-splits to be undone with just one undo operation

[banacorn]

Problem

Case split are done in 2 steps at the moment:

1. Rewrites by MakeCase from Agda

_+_ : ℕ → ℕ → ℕ  
x + y = {!   !}

_+_ : ℕ → ℕ → ℕ  
zero + y = ?
succ x + y = ?

2. Hole expansion

_+_ : ℕ → ℕ → ℕ  
zero + y = ?
succ x + y = ?

_+_ : ℕ → ℕ → ℕ  
zero + y = {!   !}
succ x + y = {!   !}

This is not ideal because it would take 2 undo operations to undo the case-split command.

---

Solution 1

VSCode.TextEditor.editor allows "undo/redo stops" to be placed or removed before or after the edit.

However, it's quite crappy) and I haven't been able to apply it successfully on case-split. And it seem to be the only API available for controlling undo/redo history :|

Solution 2

Perform case-splits in one single step. However, this would make the code a lot more convoluted. I'm less inclined to take this route and would rather wait until VS Code has a proper history API like in the Atom editor.