diff --git a/lib/js/src/Editor.bs.js b/lib/js/src/Editor.bs.js
index 020fb564..47d20d3e 100644
--- a/lib/js/src/Editor.bs.js
+++ b/lib/js/src/Editor.bs.js
@@ -209,39 +209,38 @@ function getAll($$document) {
   return $$document.getText(undefined);
 }
 
-function replace($$document, range, text) {
-  var workspaceEdit = new Vscode.WorkspaceEdit();
-  workspaceEdit.replace($$document.uri, range, text, undefined);
-  return Vscode.workspace.applyEdit(workspaceEdit);
+function replace(editor, range, text, option) {
+  return editor.edit((function (editBuilder) {
+                editBuilder.replace(range, text);
+              }), option);
 }
 
-function batchReplace($$document, replacements) {
-  var workspaceEdit = new Vscode.WorkspaceEdit();
-  replacements.forEach(function (param) {
-        workspaceEdit.replace($$document.uri, param[0], param[1], undefined);
-      });
-  return Vscode.workspace.applyEdit(workspaceEdit);
+function batchReplace(editor, replacements, option) {
+  return editor.edit((function (editBuilder) {
+                replacements.forEach(function (param) {
+                      editBuilder.replace(param[0], param[1]);
+                    });
+              }), option);
 }
 
-function insert($$document, point, text) {
-  var workspaceEdit = new Vscode.WorkspaceEdit();
-  workspaceEdit.insert($$document.uri, point, text, undefined);
-  return Vscode.workspace.applyEdit(workspaceEdit);
+function insert(editor, point, text, option) {
+  return editor.edit((function (editBuilder) {
+                editBuilder.insert(point, text);
+              }), option);
 }
 
-function batchInsert($$document, points, text) {
-  var workspaceEdit = new Vscode.WorkspaceEdit();
-  var textEdits = points.map(function (point) {
-        return Vscode.TextEdit.insert(point, text);
-      });
-  workspaceEdit.set($$document.uri, textEdits);
-  return Vscode.workspace.applyEdit(workspaceEdit);
+function batchInsert(editor, points, text, option) {
+  return editor.edit((function (editBuilder) {
+                points.forEach(function (point) {
+                      editBuilder.insert(point, text);
+                    });
+              }), option);
 }
 
-function $$delete($$document, range) {
-  var workspaceEdit = new Vscode.WorkspaceEdit();
-  workspaceEdit.delete($$document.uri, range, undefined);
-  return Vscode.workspace.applyEdit(workspaceEdit);
+function $$delete(editor, range, option) {
+  return editor.edit((function (editBuilder) {
+                editBuilder.delete(range);
+              }), option);
 }
 
 var $$Text = {
diff --git a/lib/js/src/Goal.bs.js b/lib/js/src/Goal.bs.js
index 15186382..b7b26dc6 100644
--- a/lib/js/src/Goal.bs.js
+++ b/lib/js/src/Goal.bs.js
@@ -89,7 +89,8 @@ function indentationWidth(goal, $$document) {
         ];
 }
 
-function caseSplitAux(goal, $$document) {
+function caseSplitAux(goal, editor) {
+  var $$document = editor.document;
   var range = new Vscode.Range($$document.positionAt(0), $$document.positionAt(goal.start));
   var textBeforeGoal = Editor$AgdaModeVscode.$$Text.get($$document, range);
   var nextWordBoundary = function (start, string) {
@@ -152,7 +153,8 @@ function caseSplitAux(goal, $$document) {
         ];
 }
 
-async function replaceWithLines(goal, $$document, lines) {
+async function replaceWithLines(goal, editor, lines) {
+  var $$document = editor.document;
   var match = indentationWidth(goal, $$document);
   var indentation = " ".repeat(match[0]);
   var indentedLines = indentation + lines.join("\n" + indentation);
@@ -162,7 +164,7 @@ async function replaceWithLines(goal, $$document, lines) {
   var start$1 = startLineRange.start;
   var end_ = $$document.positionAt(goal.end);
   var rangeToBeReplaced = new Vscode.Range(start$1, end_);
-  if (await Editor$AgdaModeVscode.$$Text.replace($$document, rangeToBeReplaced, indentedLines)) {
+  if (await Editor$AgdaModeVscode.$$Text.replace(editor, rangeToBeReplaced, indentedLines, undefined)) {
     return [
             rangeToBeReplaced,
             indentedLines
@@ -171,12 +173,12 @@ async function replaceWithLines(goal, $$document, lines) {
   
 }
 
-async function replaceWithLambda(goal, $$document, lines) {
-  var match = caseSplitAux(goal, $$document);
+async function replaceWithLambda(goal, editor, lines) {
+  var match = caseSplitAux(goal, editor);
   var rewriteRange = match[2];
   var indentWidth = match[1];
   var rewriteText = match[0] ? lines.join("\n" + " ".repeat(indentWidth)) : lines.join("\n" + (" ".repeat(indentWidth - 2 | 0) + "; "));
-  if (await Editor$AgdaModeVscode.$$Text.replace($$document, rewriteRange, rewriteText)) {
+  if (await Editor$AgdaModeVscode.$$Text.replace(editor, rewriteRange, rewriteText, undefined)) {
     return [
             rewriteRange,
             rewriteText
diff --git a/lib/js/src/Goals.bs.js b/lib/js/src/Goals.bs.js
index 6e24a5f6..2d63341b 100644
--- a/lib/js/src/Goals.bs.js
+++ b/lib/js/src/Goals.bs.js
@@ -65,11 +65,13 @@ function toString(goal) {
   }
 }
 
-function makeInnerRange(goal, $$document) {
+function makeInnerRange(goal, editor) {
+  var $$document = editor.document;
   return new Vscode.Range($$document.positionAt(goal.start + 2 | 0), $$document.positionAt(goal.end - 2 | 0));
 }
 
-function makeOuterRange(goal, $$document) {
+function makeOuterRange(goal, editor) {
+  var $$document = editor.document;
   return new Vscode.Range($$document.positionAt(goal.start), $$document.positionAt(goal.end));
 }
 
@@ -163,8 +165,9 @@ function toString$1(self) {
   return serialize(self).join("\n");
 }
 
-function read(goal, $$document) {
-  var innerRange = makeInnerRange(goal, $$document);
+function read(goal, editor) {
+  var innerRange = makeInnerRange(goal, editor);
+  var $$document = editor.document;
   return Editor$AgdaModeVscode.$$Text.get($$document, innerRange).trim();
 }
 
@@ -179,14 +182,14 @@ function getGoalByIndex(self, index) {
               }));
 }
 
-async function modify(self, $$document, index, f) {
+async function modify(self, editor, index, f) {
   var goal = self.goals.get(index);
   if (goal === undefined) {
     return ;
   }
-  var innerRange = makeInnerRange(goal, $$document);
-  var goalContent = read(goal, $$document);
-  await Editor$AgdaModeVscode.$$Text.replace($$document, innerRange, " " + f(goalContent) + " ");
+  var innerRange = makeInnerRange(goal, editor);
+  var goalContent = read(goal, editor);
+  await Editor$AgdaModeVscode.$$Text.replace(editor, innerRange, " " + f(goalContent) + " ", undefined);
 }
 
 async function removeBoundaryAndDestroy(self, $$document, index) {
@@ -196,7 +199,7 @@ async function removeBoundaryAndDestroy(self, $$document, index) {
   }
   var outerRange = makeOuterRange(goal, $$document);
   var content = read(goal, $$document);
-  if (await Editor$AgdaModeVscode.$$Text.replace($$document, outerRange, content)) {
+  if (await Editor$AgdaModeVscode.$$Text.replace($$document, outerRange, content, undefined)) {
     removeGoal(self, goal);
     return true;
   } else {
@@ -229,7 +232,7 @@ function setCursorByIndex(self, editor, index) {
   var $$document = editor.document;
   var position = $$document.positionAt(goal.start + 3 | 0);
   Editor$AgdaModeVscode.Cursor.set(editor, position);
-  var range = makeOuterRange(goal, $$document);
+  var range = makeOuterRange(goal, editor);
   editor.revealRange(range, undefined);
 }
 
@@ -685,7 +688,7 @@ async function scanAllGoals(self, editor, changes) {
   }
   var originalCursorPosition = Editor$AgdaModeVscode.Cursor.get(editor);
   setBusy(self);
-  await Editor$AgdaModeVscode.$$Text.batchReplace($$document, rewrites);
+  await Editor$AgdaModeVscode.$$Text.batchReplace(editor, rewrites, undefined);
   var cursorWasWithinRewrites = rewrites.some(function (param) {
         return param[0].contains(originalCursorPosition);
       });
diff --git a/lib/js/src/State/State__Command.bs.js b/lib/js/src/State/State__Command.bs.js
index 7dde6876..3f798fc5 100644
--- a/lib/js/src/State/State__Command.bs.js
+++ b/lib/js/src/State/State__Command.bs.js
@@ -104,7 +104,7 @@ async function dispatchCommand(state, command) {
                                           [Symbol.for("name")]: "Give"
                                         });
                             } else {
-                              await Goals$AgdaModeVscode.modify(state.goals, state.document, goal.index, (function (param) {
+                              await Goals$AgdaModeVscode.modify(state.goals, state.editor, goal.index, (function (param) {
                                       return expr;
                                     }));
                               return await sendAgdaRequest({
@@ -152,7 +152,7 @@ async function dispatchCommand(state, command) {
                                           [Symbol.for("name")]: "Case"
                                         });
                             } else {
-                              await Goals$AgdaModeVscode.modify(state.goals, state.document, goal$2.index, (function (param) {
+                              await Goals$AgdaModeVscode.modify(state.goals, state.editor, goal$2.index, (function (param) {
                                       return expr;
                                     }));
                               return await sendAgdaRequest({
@@ -321,7 +321,7 @@ async function dispatchCommand(state, command) {
                                         [Symbol.for("name")]: "ElaborateAndGive"
                                       });
                           } else {
-                            await Goals$AgdaModeVscode.modify(state.goals, state.document, goal$5.index, (function (param) {
+                            await Goals$AgdaModeVscode.modify(state.goals, state.editor, goal$5.index, (function (param) {
                                     return expr;
                                   }));
                             return await sendAgdaRequest({
diff --git a/lib/js/src/State/State__InputMethod.bs.js b/lib/js/src/State/State__InputMethod.bs.js
index a5cf0bb7..cc901a53 100644
--- a/lib/js/src/State/State__InputMethod.bs.js
+++ b/lib/js/src/State/State__InputMethod.bs.js
@@ -33,7 +33,7 @@ async function handle(state, output) {
                     [Symbol.for("name")]: "Update"
                   });
       }
-      await Editor$AgdaModeVscode.$$Text.batchReplace(state.document, kind._0);
+      await Editor$AgdaModeVscode.$$Text.batchReplace(state.editor, kind._0, undefined);
       return kind._1();
     }
   };
@@ -298,7 +298,7 @@ async function insertChar$1(state, $$char) {
     case "Editor" :
         var $$char$1 = $$char.charAt(0);
         var positions = Editor$AgdaModeVscode.Cursor.getMany(state.editor);
-        await Editor$AgdaModeVscode.$$Text.batchInsert(state.document, positions, $$char$1);
+        await Editor$AgdaModeVscode.$$Text.batchInsert(state.editor, positions, $$char$1, undefined);
         return Editor$AgdaModeVscode.focus(state.document);
     case "Prompt" :
         return await insertChar(state, $$char);
diff --git a/lib/js/src/State/State__Response.bs.js b/lib/js/src/State/State__Response.bs.js
index b0879053..cbcb7e3d 100644
--- a/lib/js/src/State/State__Response.bs.js
+++ b/lib/js/src/State/State__Response.bs.js
@@ -271,7 +271,7 @@ async function handle$1(state, dispatchCommand, response) {
             }
             if (typeof give !== "object") {
               if (give === "GiveParen") {
-                await Goals$AgdaModeVscode.modify(state.goals, state.document, index, (function (content) {
+                await Goals$AgdaModeVscode.modify(state.goals, state.editor, index, (function (content) {
                         return "(" + content + ")";
                       }));
               }
@@ -279,7 +279,7 @@ async function handle$1(state, dispatchCommand, response) {
             } else {
               var match = Goal$AgdaModeVscode.indentationWidth(goal, state.document);
               var indented = indent(Parser$AgdaModeVscode.unescapeEOL(give._0), 2 + match[0] | 0);
-              await Goals$AgdaModeVscode.modify(state.goals, state.document, index, (function (param) {
+              await Goals$AgdaModeVscode.modify(state.goals, state.editor, index, (function (param) {
                       return indented;
                     }));
               var goalPositionsRelative = Goals$AgdaModeVscode.parseGoalPositionsFromRefine(indented);
@@ -298,7 +298,7 @@ async function handle$1(state, dispatchCommand, response) {
               }
               Goals$AgdaModeVscode.addGoalPositions(state.goals, goalPositionsAbsolute);
             }
-            if (await Goals$AgdaModeVscode.removeBoundaryAndDestroy(state.goals, state.document, index)) {
+            if (await Goals$AgdaModeVscode.removeBoundaryAndDestroy(state.goals, state.editor, index)) {
               return ;
             } else {
               return await State__View$AgdaModeVscode.Panel.display(state, {
@@ -318,7 +318,7 @@ async function handle$1(state, dispatchCommand, response) {
                         }, [Item$AgdaModeVscode.plainText("Failed to remember the goal being split")]);
             }
             var result;
-            result = response._0 === "Function" ? await Goal$AgdaModeVscode.replaceWithLines(goal$1, state.document, lines) : await Goal$AgdaModeVscode.replaceWithLambda(goal$1, state.document, lines);
+            result = response._0 === "Function" ? await Goal$AgdaModeVscode.replaceWithLines(goal$1, state.editor, lines) : await Goal$AgdaModeVscode.replaceWithLambda(goal$1, state.editor, lines);
             if (result !== undefined) {
               Goals$AgdaModeVscode.removeGoalByIndex(state.goals, goal$1.index);
               Goal$AgdaModeVscode.placeCursorAtFirstNewGoal(state.editor, result[0], result[1]);
@@ -338,7 +338,7 @@ async function handle$1(state, dispatchCommand, response) {
               return async function () {
                 var goal = Goals$AgdaModeVscode.getGoalByIndex(state.goals, index);
                 if (goal !== undefined) {
-                  await Goals$AgdaModeVscode.modify(state.goals, state.document, index, (function (param) {
+                  await Goals$AgdaModeVscode.modify(state.goals, state.editor, index, (function (param) {
                           return solution;
                         }));
                   return await sendAgdaRequest({
diff --git a/lib/js/test/tests/Test__EditorIM.bs.js b/lib/js/test/tests/Test__EditorIM.bs.js
index d45c5885..43cfe309 100644
--- a/lib/js/test/tests/Test__EditorIM.bs.js
+++ b/lib/js/test/tests/Test__EditorIM.bs.js
@@ -28,7 +28,7 @@ function acquire(setup) {
 
 async function cleanup(setup) {
   var range = new Vscode.Range(new Vscode.Position(0, 0), new Vscode.Position(100, 0));
-  await Editor$AgdaModeVscode.$$Text.replace(setup.editor.document, range, "");
+  await Editor$AgdaModeVscode.$$Text.replace(setup.editor, range, "", undefined);
 }
 
 async function wait(setup) {
@@ -69,7 +69,7 @@ async function deactivate(setup) {
 async function insertChar(setup, $$char) {
   var promise = waitMany(setup, 2);
   var positions = Editor$AgdaModeVscode.Cursor.getMany(setup.editor);
-  var succeed = await Editor$AgdaModeVscode.$$Text.batchInsert(setup.editor.document, positions, $$char);
+  var succeed = await Editor$AgdaModeVscode.$$Text.batchInsert(setup.editor, positions, $$char, undefined);
   if (succeed) {
     return await promise;
   }
@@ -105,7 +105,7 @@ async function backspace(setup) {
   var end_ = Editor$AgdaModeVscode.Cursor.get(setup.editor);
   var start = end_.translate(0, -1);
   var range = new Vscode.Range(start, end_);
-  var succeed = await Editor$AgdaModeVscode.$$Text.$$delete(setup.editor.document, range);
+  var succeed = await Editor$AgdaModeVscode.$$Text.$$delete(setup.editor, range, undefined);
   if (succeed) {
     return await promise;
   }
@@ -876,7 +876,7 @@ describe("Input Method (Editor)", (function () {
                         var setup$1 = acquire(setup);
                         var positions = [new Vscode.Position(0, 3)];
                         var $$document = setup$1.editor.document;
-                        await Editor$AgdaModeVscode.$$Text.insert($$document, new Vscode.Position(0, 0), "123");
+                        await Editor$AgdaModeVscode.$$Text.insert(setup$1.editor, new Vscode.Position(0, 0), "123", undefined);
                         var log = await activate(setup$1, positions, undefined);
                         Curry._3(Assert.deepStrictEqual, ["Activate"], log, undefined);
                         var log$1 = await insertChar(setup$1, "a");
@@ -1148,7 +1148,7 @@ describe("Input Method (Editor)", (function () {
                         ];
                         var setup$1 = acquire(setup);
                         var $$document = setup$1.editor.document;
-                        await Editor$AgdaModeVscode.$$Text.insert($$document, new Vscode.Position(0, 0), "\n\n\n");
+                        await Editor$AgdaModeVscode.$$Text.insert(setup$1.editor, new Vscode.Position(0, 0), "\n\n\n", undefined);
                         var log = await activate(setup$1, positions, undefined);
                         Curry._3(Assert.deepStrictEqual, ["Activate"], log, undefined);
                         var log$1 = await insertChar(setup$1, "b");
@@ -1289,7 +1289,7 @@ describe("Input Method (Editor)", (function () {
                         ];
                         var setup$1 = acquire(setup);
                         var $$document = setup$1.editor.document;
-                        await Editor$AgdaModeVscode.$$Text.insert($$document, new Vscode.Position(0, 0), "123\n123\n123\n123");
+                        await Editor$AgdaModeVscode.$$Text.insert(setup$1.editor, new Vscode.Position(0, 0), "123\n123\n123\n123", undefined);
                         var log = await activate(setup$1, positions, undefined);
                         Curry._3(Assert.deepStrictEqual, ["Activate"], log, undefined);
                         var log$1 = await insertChar(setup$1, "a");
diff --git a/lib/js/test/tests/Test__Give.bs.js b/lib/js/test/tests/Test__Give.bs.js
index 16fa3a5f..080d9a47 100644
--- a/lib/js/test/tests/Test__Give.bs.js
+++ b/lib/js/test/tests/Test__Give.bs.js
@@ -22,7 +22,7 @@ describe("agda-mode.give", (function () {
             });
         it("should be responded with correct responses", (async function () {
                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Give.agda");
-                await Editor$AgdaModeVscode.$$Text.insert(ctx.state.document, new Vscode.Position(7, 14), "y");
+                await Editor$AgdaModeVscode.$$Text.insert(ctx.state.editor, new Vscode.Position(7, 14), "y", undefined);
                 var responses = await State__Connection$AgdaModeVscode.sendRequestAndCollectResponses(ctx.state, {
                       TAG: "Give",
                       _0: {
diff --git a/lib/js/test/tests/Test__Goals.bs.js b/lib/js/test/tests/Test__Goals.bs.js
index 37ef7966..9948272a 100644
--- a/lib/js/test/tests/Test__Goals.bs.js
+++ b/lib/js/test/tests/Test__Goals.bs.js
@@ -41,7 +41,7 @@ describe("Goals", (function () {
                       }));
                 it("should translate goals on an insertion immediately before a goal", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.insert(ctx.state.document, new Vscode.Position(8, 18), " ");
+                        await Editor$AgdaModeVscode.$$Text.insert(ctx.state.editor, new Vscode.Position(8, 18), " ", undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:20-27)",
@@ -53,7 +53,7 @@ describe("Goals", (function () {
                       }));
                 it("should translate goals on an insertion immediately after a goal", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.insert(ctx.state.document, new Vscode.Position(8, 25), " ");
+                        await Editor$AgdaModeVscode.$$Text.insert(ctx.state.editor, new Vscode.Position(8, 25), " ", undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:19-26)",
@@ -65,7 +65,7 @@ describe("Goals", (function () {
                       }));
                 it("should destroy a goal after it has been completely deleted", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26)));
+                        await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26)), undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:19-26)",
@@ -76,7 +76,7 @@ describe("Goals", (function () {
                       }));
                 it("should destroy a goal after it has been completely replaced 1", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26)), "       ");
+                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26)), "       ", undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:19-26)",
@@ -87,7 +87,7 @@ describe("Goals", (function () {
                       }));
                 it("should destroy a goal after it has been completely replaced 2", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.document, new Vscode.Range(new Vscode.Position(10, 17), new Vscode.Position(10, 26)), "::DD");
+                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.editor, new Vscode.Range(new Vscode.Position(10, 17), new Vscode.Position(10, 26)), "::DD", undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:19-26)",
@@ -98,7 +98,7 @@ describe("Goals", (function () {
                       }));
                 it("should only resize a goal after its content has been edited", (async function () {
                         var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 22), new Vscode.Position(9, 23)), ":D");
+                        await Editor$AgdaModeVscode.$$Text.replace(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 22), new Vscode.Position(9, 23)), ":D", undefined);
                         Curry._3(Assert.deepStrictEqual, Goals$AgdaModeVscode.serialize(ctx.state.goals), [
                               "#0 [8:12-19)",
                               "#1 [9:19-26)",
@@ -111,7 +111,7 @@ describe("Goals", (function () {
                 describe.skip("Restore hole damaged boundaries", (function () {
                         it("should protect against a backspace on the right boundary", (async function () {
                                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 25), new Vscode.Position(9, 26)));
+                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 25), new Vscode.Position(9, 26)), undefined);
                                 await Test__Util$AgdaModeVscode.AgdaMode.quit(ctx);
                                 var range = new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26));
                                 var actual = Editor$AgdaModeVscode.$$Text.get(ctx.state.document, range);
@@ -125,7 +125,7 @@ describe("Goals", (function () {
                               }));
                         it("should protect against a deletion on the right boundary", (async function () {
                                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 24), new Vscode.Position(9, 25)));
+                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 24), new Vscode.Position(9, 25)), undefined);
                                 await Test__Util$AgdaModeVscode.AgdaMode.quit(ctx);
                                 var range = new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26));
                                 var actual = Editor$AgdaModeVscode.$$Text.get(ctx.state.document, range);
@@ -139,7 +139,7 @@ describe("Goals", (function () {
                               }));
                         it("should protect against a backspace on the left boundary", (async function () {
                                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 20), new Vscode.Position(9, 21)));
+                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 20), new Vscode.Position(9, 21)), undefined);
                                 await Test__Util$AgdaModeVscode.AgdaMode.quit(ctx);
                                 var range = new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26));
                                 var actual = Editor$AgdaModeVscode.$$Text.get(ctx.state.document, range);
@@ -153,7 +153,7 @@ describe("Goals", (function () {
                               }));
                         it("should protect against a deletion on the left boundary", (async function () {
                                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Goals.agda");
-                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 20)));
+                                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 20)), undefined);
                                 await Test__Util$AgdaModeVscode.AgdaMode.quit(ctx);
                                 var range = new Vscode.Range(new Vscode.Position(9, 19), new Vscode.Position(9, 26));
                                 var actual = Editor$AgdaModeVscode.$$Text.get(ctx.state.document, range);
diff --git a/lib/js/test/tests/Test__HelperFunctionType.bs.js b/lib/js/test/tests/Test__HelperFunctionType.bs.js
index 87d8f748..3e632629 100644
--- a/lib/js/test/tests/Test__HelperFunctionType.bs.js
+++ b/lib/js/test/tests/Test__HelperFunctionType.bs.js
@@ -26,7 +26,7 @@ function run(normalization) {
             return ;
           }
           var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(filename);
-          await Editor$AgdaModeVscode.$$Text.insert(ctx.state.document, new Vscode.Position(7, 14), "y");
+          await Editor$AgdaModeVscode.$$Text.insert(ctx.state.editor, new Vscode.Position(7, 14), "y", undefined);
           var responses = await State__Connection$AgdaModeVscode.sendRequestAndCollectResponses(ctx.state, {
                 TAG: "HelperFunctionType",
                 _0: normalization,
diff --git a/lib/js/test/tests/Test__Highlighting.bs.js b/lib/js/test/tests/Test__Highlighting.bs.js
index 6a24a3d6..ffccf1d3 100644
--- a/lib/js/test/tests/Test__Highlighting.bs.js
+++ b/lib/js/test/tests/Test__Highlighting.bs.js
@@ -22,7 +22,7 @@ describe("Highlighting", (function () {
             });
         it("should work after inserting a newline", (async function () {
                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Issue180.agda");
-                await Editor$AgdaModeVscode.$$Text.insert(ctx.state.document, new Vscode.Position(6, 0), "\n");
+                await Editor$AgdaModeVscode.$$Text.insert(ctx.state.editor, new Vscode.Position(6, 0), "\n", undefined);
                 var expected = [
                   "(7:0-3) function",
                   "(7:6-7) type",
@@ -38,7 +38,7 @@ describe("Highlighting", (function () {
               }));
         it("should work after deleting an empty line", (async function () {
                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Issue180.agda");
-                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(5, 0), new Vscode.Position(6, 0)));
+                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(5, 0), new Vscode.Position(6, 0)), undefined);
                 var expected = [
                   "(5:0-3) function",
                   "(5:6-7) type",
@@ -54,7 +54,7 @@ describe("Highlighting", (function () {
               }));
         it("should work after deleting an existing line", (async function () {
                 var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad("Issue180.agda");
-                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.document, new Vscode.Range(new Vscode.Position(5, 0), new Vscode.Position(7, 0)));
+                await Editor$AgdaModeVscode.$$Text.$$delete(ctx.state.editor, new Vscode.Range(new Vscode.Position(5, 0), new Vscode.Position(7, 0)), undefined);
                 var expected = [
                   "(5:0-1) variable",
                   "(5:2-3) function",
diff --git a/lib/js/test/tests/Test__UndoRedoHistory.bs.js b/lib/js/test/tests/Test__UndoRedoHistory.bs.js
new file mode 100644
index 00000000..004ac64f
--- /dev/null
+++ b/lib/js/test/tests/Test__UndoRedoHistory.bs.js
@@ -0,0 +1,31 @@
+// Generated by ReScript, PLEASE EDIT WITH CARE
+'use strict';
+
+var Curry = require("rescript/lib/js/curry.js");
+var Assert = require("assert");
+var Vscode = require("vscode");
+var Test__Util$AgdaModeVscode = require("./Test__Util.bs.js");
+
+describe.skip("Undo/Redo History", (function () {
+        this.timeout(4000);
+        var filename = "CaseSplit.agda";
+        var fileContent = {
+          contents: ""
+        };
+        beforeEach(async function () {
+              fileContent.contents = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset(filename));
+            });
+        afterEach(async function () {
+              return await Test__Util$AgdaModeVscode.$$File.write(Test__Util$AgdaModeVscode.Path.asset(filename), fileContent.contents);
+            });
+        it("shoule make case split a single transaction", (async function () {
+                var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(filename);
+                await Test__Util$AgdaModeVscode.AgdaMode.$$case(ctx, new Vscode.Position(8, 11), "x");
+                await Vscode.commands.executeCommand("undo");
+                var actual = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset("CaseSplit.agda"));
+                var expected = fileContent.contents;
+                return Curry._3(Assert.deepStrictEqual, actual, expected, undefined);
+              }));
+      }));
+
+/*  Not a pure module */
diff --git a/lib/js/test/tests/Test__Util.bs.js b/lib/js/test/tests/Test__Util.bs.js
index b73b761b..968927aa 100644
--- a/lib/js/test/tests/Test__Util.bs.js
+++ b/lib/js/test/tests/Test__Util.bs.js
@@ -46,7 +46,7 @@ async function write(fileName, content) {
   var $$document = editor.document;
   var lineCount = $$document.lineCount;
   var replaceRange = new Vscode.Range(new Vscode.Position(0, 0), new Vscode.Position(lineCount, 0));
-  var succeed = await Editor$AgdaModeVscode.$$Text.replace($$document, replaceRange, content);
+  var succeed = await Editor$AgdaModeVscode.$$Text.replace(editor, replaceRange, content, undefined);
   if (succeed) {
     await $$document.save();
     return ;
@@ -465,7 +465,7 @@ async function quit(self) {
 
 async function $$case(self, cursor, payload) {
   var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(self.filepath), undefined);
-  var succeed = await Editor$AgdaModeVscode.$$Text.insert(self.state.document, cursor, payload);
+  var succeed = await Editor$AgdaModeVscode.$$Text.insert(self.state.editor, cursor, payload, undefined);
   if (!succeed) {
     throw {
           RE_EXN_ID: "Failure",
@@ -540,7 +540,7 @@ async function execute$1(self, command, cursor, payload) {
   if (cursor !== undefined) {
     var cursor$1 = Caml_option.valFromOption(cursor);
     if (payload !== undefined) {
-      await Editor$AgdaModeVscode.$$Text.insert(self.state.document, cursor$1, payload);
+      await Editor$AgdaModeVscode.$$Text.insert(self.state.editor, cursor$1, payload, undefined);
     }
     Editor$AgdaModeVscode.Cursor.set(editor, cursor$1);
   }
diff --git a/src/Editor.res b/src/Editor.res
index 2c0c101c..3a4898f0 100644
--- a/src/Editor.res
+++ b/src/Editor.res
@@ -146,46 +146,33 @@ module Text = {
   let get = (document, range) => document->TextDocument.getText(Some(range))
   let getAll = document => document->TextDocument.getText(None)
 
-  let replace = (document, range, text) => {
-    let workspaceEdit = WorkspaceEdit.make()
-    workspaceEdit->WorkspaceEdit.replace(document->TextDocument.uri, range, text, None)
-    Workspace.applyEdit(workspaceEdit)
-  }
-  let batchReplace = (document, replacements) => {
-    let workspaceEdit = WorkspaceEdit.make()
-    replacements->Array.forEach(((range, text)) =>
-      workspaceEdit->WorkspaceEdit.replace(document->TextDocument.uri, range, text, None)
+  let replace = (editor, range, text, ~option=?) => {
+    editor->VSCode.TextEditor.edit(
+      editBuilder => editBuilder->TextEditorEdit.replaceAtRange(range, text),
+      option,
     )
-    Workspace.applyEdit(workspaceEdit)
   }
-  // let batchReplace' = (editor, replacements) => {
-  //   editor->TextEditor.edit(editBuilder => {
-  //     replacements->Array.forEach(((range, text)) =>
-  //       editBuilder->TextEditorEdit.replaceAtRange(range, text)
-  //     )
-  //   }, None)
-  // }
-
-  let insert = (document, point, text) => {
-    let workspaceEdit = WorkspaceEdit.make()
-    workspaceEdit->WorkspaceEdit.insert(document->TextDocument.uri, point, text, None)
-    Workspace.applyEdit(workspaceEdit)
+  let batchReplace = (editor, replacements, ~option=?) => {
+    editor->TextEditor.edit(editBuilder => {
+      replacements->Array.forEach(((range, text)) =>
+        editBuilder->TextEditorEdit.replaceAtRange(range, text)
+      )
+    }, option)
+  }
+
+  let insert = (editor, point, text, ~option=?) => {
+    editor->VSCode.TextEditor.edit(
+      editBuilder => editBuilder->TextEditorEdit.insert(point, text),
+      option,
+    )
   }
-  let batchInsert = (document, points, text) => {
-    let workspaceEdit = WorkspaceEdit.make()
-    let textEdits = points->Array.map(point => TextEdit.insert(point, text))
-    workspaceEdit->WorkspaceEdit.set(document->TextDocument.uri, textEdits)
-    Workspace.applyEdit(workspaceEdit)
+  let batchInsert = (editor, points, text, ~option=?) => {
+    editor->VSCode.TextEditor.edit(editBuilder => {
+      points->Array.forEach(point => editBuilder->TextEditorEdit.insert(point, text))
+    }, option)
   }
-  // let batchInsert' = (editor, points, text) => {
-  //   editor->TextEditor.edit(editBuilder => {
-  //     points->Array.forEach(point => editBuilder->TextEditorEdit.insert(point, text))
-  //   }, None)
-  // }
-  let delete = (document, range) => {
-    let workspaceEdit = WorkspaceEdit.make()
-    workspaceEdit->WorkspaceEdit.delete(document->TextDocument.uri, range, None)
-    Workspace.applyEdit(workspaceEdit)
+  let delete = (editor, range, ~option=?) => {
+    editor->VSCode.TextEditor.edit(editBuilder => editBuilder->TextEditorEdit.delete(range), option)
   }
 }
 
diff --git a/src/Goal.res b/src/Goal.res
index d0ff6068..cbd9f866 100644
--- a/src/Goal.res
+++ b/src/Goal.res
@@ -17,12 +17,12 @@ module type Module = {
   // for case splitting
   let replaceWithLines: (
     t,
-    VSCode.TextDocument.t,
+    VSCode.TextEditor.t,
     array<string>,
   ) => promise<option<(VSCode.Range.t, string)>>
   let replaceWithLambda: (
     t,
-    VSCode.TextDocument.t,
+    VSCode.TextEditor.t,
     array<string>,
   ) => promise<option<(VSCode.Range.t, string)>>
   let placeCursorAtFirstNewGoal: (VSCode.TextEditor.t, VSCode.Range.t, string) => unit
@@ -138,7 +138,8 @@ module Module: Module = {
   //      λ where x → ?
   //        ^------------------- the "where" token
 
-  let caseSplitAux = (goal, document) => {
+  let caseSplitAux = (goal, editor) => {
+    let document = VSCode.TextEditor.document(editor)
     let textBeforeGoal = {
       let range = VSCode.Range.make(
         VSCode.TextDocument.positionAt(document, 0),
@@ -233,8 +234,9 @@ module Module: Module = {
 
   // replace and insert one or more lines of content at the goal
   // usage: case split
-  let replaceWithLines = async (goal, document, lines) => {
+  let replaceWithLines = async (goal, editor, lines) => {
     // get the width of indentation from the first line of the goal
+    let document = VSCode.TextEditor.document(editor)
     let (indentWidth, _, _) = indentationWidth(goal, document)
     let indentation = String.repeat(" ", indentWidth)
     let indentedLines = indentation ++ lines->Array.join("\n" ++ indentation)
@@ -247,7 +249,10 @@ module Module: Module = {
 
     let end_ = VSCode.TextDocument.positionAt(document, goal.end)
     let rangeToBeReplaced = VSCode.Range.make(start, end_)
-    if await Editor.Text.replace(document, rangeToBeReplaced, indentedLines) {
+
+    // don't add a "undo stop" after this operation
+    // so that we can lump this operation with the next one (hole expansion), making case split undoable
+    if await Editor.Text.replace(editor, rangeToBeReplaced, indentedLines) {
       Some(rangeToBeReplaced, indentedLines)
     } else {
       None
@@ -264,14 +269,14 @@ module Module: Module = {
   //  2.  λ where
   //          x → ?
   //          y → ?
-  let replaceWithLambda = async (goal, document, lines) => {
-    let (inWhereClause, indentWidth, rewriteRange) = caseSplitAux(goal, document)
+  let replaceWithLambda = async (goal, editor, lines) => {
+    let (inWhereClause, indentWidth, rewriteRange) = caseSplitAux(goal, editor)
     let rewriteText = if inWhereClause {
       lines->Array.join("\n" ++ String.repeat(" ", indentWidth))
     } else {
       lines->Array.join("\n" ++ (String.repeat(" ", indentWidth - 2) ++ "; "))
     }
-    if await Editor.Text.replace(document, rewriteRange, rewriteText) {
+    if await Editor.Text.replace(editor, rewriteRange, rewriteText) {
       Some(rewriteRange, rewriteText)
     } else {
       None
diff --git a/src/Goals.res b/src/Goals.res
index 61101991..f20e596a 100644
--- a/src/Goals.res
+++ b/src/Goals.res
@@ -17,8 +17,8 @@ module type Module = {
 
   let getGoalByIndex: (t, index) => option<Goal.t>
 
-  let modify: (t, VSCode.TextDocument.t, index, string => string) => promise<unit>
-  let removeBoundaryAndDestroy: (t, VSCode.TextDocument.t, index) => promise<bool>
+  let modify: (t, VSCode.TextEditor.t, index, string => string) => promise<unit>
+  let removeBoundaryAndDestroy: (t, VSCode.TextEditor.t, index) => promise<bool>
   // get the goal at the cursor position
   let getGoalAtCursor: (t, VSCode.TextEditor.t) => option<Goal.t>
   let setCursorByIndex: (t, VSCode.TextEditor.t, int) => unit
@@ -131,17 +131,21 @@ module Module: Module = {
           )})`
       }
 
-    let makeInnerRange = (goal, document) =>
+    let makeInnerRange = (goal, editor) => {
+      let document = VSCode.TextEditor.document(editor)
       VSCode.Range.make(
         VSCode.TextDocument.positionAt(document, goal.start + 2),
         VSCode.TextDocument.positionAt(document, goal.end - 2),
       )
+    }
 
-    let makeOuterRange = (goal, document) =>
+    let makeOuterRange = (goal, editor) => {
+      let document = VSCode.TextEditor.document(editor)
       VSCode.Range.make(
         VSCode.TextDocument.positionAt(document, goal.start),
         VSCode.TextDocument.positionAt(document, goal.end),
       )
+    }
   }
 
   type t = {
@@ -256,8 +260,9 @@ module Module: Module = {
 
   let getInternalGoalByIndex = (self, index) => self.goals->Map.get(index)
 
-  let read = (goal, document) => {
-    let innerRange = InternalGoal.makeInnerRange(goal, document)
+  let read = (goal, editor) => {
+    let innerRange = InternalGoal.makeInnerRange(goal, editor)
+    let document = VSCode.TextEditor.document(editor)
     Editor.Text.get(document, innerRange)->String.trim
   }
 
@@ -273,12 +278,12 @@ module Module: Module = {
       }
     })
 
-  let modify = async (self, document, index, f) =>
+  let modify = async (self, editor, index, f) =>
     switch getInternalGoalByIndex(self, index) {
     | Some(goal) =>
-      let innerRange = InternalGoal.makeInnerRange(goal, document)
-      let goalContent = read(goal, document)
-      let _ = await Editor.Text.replace(document, innerRange, " " ++ f(goalContent) ++ " ")
+      let innerRange = InternalGoal.makeInnerRange(goal, editor)
+      let goalContent = read(goal, editor)
+      let _ = await Editor.Text.replace(editor, innerRange, " " ++ f(goalContent) ++ " ")
     | None => ()
     }
 
@@ -329,7 +334,7 @@ module Module: Module = {
       let position = VSCode.TextDocument.positionAt(document, goal.start + 3)
       Editor.Cursor.set(editor, position)
       // scroll to that part of the document
-      let range = InternalGoal.makeOuterRange(goal, document)
+      let range = InternalGoal.makeOuterRange(goal, editor)
       editor->VSCode.TextEditor.revealRange(range, None)
     }
 
@@ -698,7 +703,9 @@ module Module: Module = {
       let originalCursorPosition = Editor.Cursor.get(editor)
       // set busy
       setBusy(self)
-      let _ = await Editor.Text.batchReplace(document, rewrites)
+
+      // add a "undo stop" after this operation
+      let _ = await Editor.Text.batchReplace(editor, rewrites)
 
       // place the cursor inside a hole if it was there before the rewrite
       let cursorWasWithinRewrites =
diff --git a/src/State/State__Command.res b/src/State/State__Command.res
index 7bbc6fd4..6aa0dab7 100644
--- a/src/State/State__Command.res
+++ b/src/State/State__Command.res
@@ -75,7 +75,7 @@ let rec dispatchCommand = async (state: State.t, command): unit => {
             if expr == "" {
               await sendAgdaRequest(Give(goal))
             } else {
-              await state.goals->Goals.modify(state.document, goal.index, _ => expr)
+              await state.goals->Goals.modify(state.editor, goal.index, _ => expr)
               await sendAgdaRequest(Give(goal))
             },
         )
@@ -107,7 +107,7 @@ let rec dispatchCommand = async (state: State.t, command): unit => {
               if expr == "" {
                 await sendAgdaRequest(ElaborateAndGive(normalization, expr, goal))
               } else {
-                await state.goals->Goals.modify(state.document, goal.index, _ => expr)
+                await state.goals->Goals.modify(state.editor, goal.index, _ => expr)
                 await sendAgdaRequest(ElaborateAndGive(normalization, expr, goal))
               },
           )
@@ -145,7 +145,7 @@ let rec dispatchCommand = async (state: State.t, command): unit => {
               await sendAgdaRequest(Case(goal))
             } else {
               // place the queried expression in the goal
-              await state.goals->Goals.modify(state.document, goal.index, _ => expr)
+              await state.goals->Goals.modify(state.editor, goal.index, _ => expr)
               await sendAgdaRequest(Case(goal))
             },
         )
diff --git a/src/State/State__InputMethod.res b/src/State/State__InputMethod.res
index 43e27ff0..0e75fc28 100644
--- a/src/State/State__InputMethod.res
+++ b/src/State/State__InputMethod.res
@@ -28,7 +28,7 @@ module Module: Module = {
         | UpdateView(sequence, translation, index) =>
           await State__View.Panel.updateIM(state, Update(sequence, translation, index))
         | Rewrite(replacements, resolve) =>
-          let _ = await Editor.Text.batchReplace(state.document, replacements)
+          let _ = await Editor.Text.batchReplace(state.editor, replacements)
           resolve()
         | Activate =>
           await State__View.Panel.display(state, Plain("Unicode input mode"), [])
@@ -245,7 +245,7 @@ module Module: Module = {
       let char = String.charAt(char, 0)
       let positions = Editor.Cursor.getMany(state.editor)
 
-      let _ = await state.document->Editor.Text.batchInsert(positions, char)
+      let _ = await state.editor->Editor.Text.batchInsert(positions, char)
       Editor.focus(state.document)
     | Prompt => await PromptIM.insertChar(state, char)
     | None => ()
diff --git a/src/State/State__Response.res b/src/State/State__Response.res
index c56a8cd8..3aafc1e0 100644
--- a/src/State/State__Response.res
+++ b/src/State/State__Response.res
@@ -154,7 +154,7 @@ let rec handle = async (
       | Some(goal) =>
         switch give {
         | GiveParen =>
-          await state.goals->Goals.modify(state.document, index, content => "(" ++ content ++ ")")
+          await state.goals->Goals.modify(state.editor, index, content => "(" ++ content ++ ")")
         | GiveNoParen => () // no need to modify the document
         | GiveString(content) =>
           let (indentationWidth, _text, _) = Goal.indentationWidth(goal, state.document)
@@ -169,7 +169,7 @@ let rec handle = async (
           let indented = Parser.unescapeEOL(content)->indent(defaultIndentation + indentationWidth)
 
           // modify the document
-          await state.goals->Goals.modify(state.document, index, _ => indented)
+          await state.goals->Goals.modify(state.editor, index, _ => indented)
 
           // add goal positions
           let goalPositionsRelative = Goals.parseGoalPositionsFromRefine(indented)
@@ -181,7 +181,7 @@ let rec handle = async (
           state.goals->Goals.addGoalPositions(goalPositionsAbsolute)
         }
 
-        if await Goals.removeBoundaryAndDestroy(state.goals, state.document, index) {
+        if await Goals.removeBoundaryAndDestroy(state.goals, state.editor, index) {
           ()
         } else {
           await State__View.Panel.display(
@@ -202,8 +202,8 @@ let rec handle = async (
         )
       | Some(goal) =>
         let result = switch makeCaseType {
-        | Function => await Goal.replaceWithLines(goal, state.document, lines)
-        | ExtendedLambda => await Goal.replaceWithLambda(goal, state.document, lines)
+        | Function => await Goal.replaceWithLines(goal, state.editor, lines)
+        | ExtendedLambda => await Goal.replaceWithLambda(goal, state.editor, lines)
         }
 
         switch result {
@@ -227,7 +227,7 @@ let rec handle = async (
         | None => ()
         | Some(goal) =>
           // modify the goal content
-          await Goals.modify(state.goals, state.document, index, _ => solution)
+          await Goals.modify(state.goals, state.editor, index, _ => solution)
           // send the give request to Agda
           await sendAgdaRequest(Give(goal))
         }
diff --git a/test/tests/Test__EditorIM.res b/test/tests/Test__EditorIM.res
index 4c8f409b..8836022d 100644
--- a/test/tests/Test__EditorIM.res
+++ b/test/tests/Test__EditorIM.res
@@ -14,7 +14,7 @@ let acquire = setup =>
 
 let cleanup = async setup => {
   let range = VSCode.Range.make(VSCode.Position.make(0, 0), VSCode.Position.make(100, 0))
-  let _ = await setup.editor->VSCode.TextEditor.document->Editor.Text.replace(range, "")
+  let _ = await setup.editor->Editor.Text.replace(range, "")
 }
 
 module IM = {
@@ -59,10 +59,7 @@ module IM = {
 
     let positions = Editor.Cursor.getMany(setup.editor)
 
-    let succeed =
-      await setup.editor
-      ->VSCode.TextEditor.document
-      ->Editor.Text.batchInsert(positions, char)
+    let succeed = await setup.editor->Editor.Text.batchInsert(positions, char)
 
     if succeed {
       await promise
@@ -104,10 +101,7 @@ module IM = {
     let end_ = Editor.Cursor.get(setup.editor)
     let start = end_->VSCode.Position.translate(0, -1)
     let range = VSCode.Range.make(start, end_)
-    let succeed =
-      await setup.editor
-      ->VSCode.TextEditor.document
-      ->Editor.Text.delete(range)
+    let succeed = await setup.editor->Editor.Text.delete(range)
 
     if succeed {
       await promise
@@ -431,7 +425,7 @@ describe("Input Method (Editor)", () => {
         let setup = acquire(setup)
         let positions = [VSCode.Position.make(0, 3)]
         let document = setup.editor->VSCode.TextEditor.document
-        let _ = await document->Editor.Text.insert(VSCode.Position.make(0, 0), "123")
+        let _ = await setup.editor->Editor.Text.insert(VSCode.Position.make(0, 0), "123")
         let log = await IM.activate(setup, ~positions, ())
         Assert.deepStrictEqual([IM.Log.Activate], log)
         let log = await IM.insertChar(setup, "a")
@@ -557,7 +551,7 @@ describe("Input Method (Editor)", () => {
 
         let setup = acquire(setup)
         let document = setup.editor->VSCode.TextEditor.document
-        let _ = await document->Editor.Text.insert(VSCode.Position.make(0, 0), "\n\n\n")
+        let _ = await setup.editor->Editor.Text.insert(VSCode.Position.make(0, 0), "\n\n\n")
         let log = await IM.activate(setup, ~positions, ())
         Assert.deepStrictEqual([IM.Log.Activate], log)
         let log = await IM.insertChar(setup, "b")
@@ -612,14 +606,21 @@ describe("Input Method (Editor)", () => {
 
         let setup = acquire(setup)
         let document = setup.editor->VSCode.TextEditor.document
-        let _ = await document->Editor.Text.insert(VSCode.Position.make(0, 0), "123\n123\n123\n123")
+        let _ =
+          await setup.editor->Editor.Text.insert(VSCode.Position.make(0, 0), "123\n123\n123\n123")
         let log = await IM.activate(setup, ~positions, ())
         Assert.deepStrictEqual([IM.Log.Activate], log)
         let log = await IM.insertChar(setup, "a")
-        Assert.deepStrictEqual([IM.Log.RewriteIssued([]), IM.Log.UpdateView, IM.Log.RewriteApplied], log)
+        Assert.deepStrictEqual(
+          [IM.Log.RewriteIssued([]), IM.Log.UpdateView, IM.Log.RewriteApplied],
+          log,
+        )
         Assert.equal("a123\n1a23\n12a3\n123a", Editor.Text.getAll(document)->replaceCRLF)
         let log = await IM.insertChar(setup, "n")
-        Assert.deepStrictEqual([IM.Log.RewriteIssued([]), IM.Log.UpdateView, IM.Log.RewriteApplied], log)
+        Assert.deepStrictEqual(
+          [IM.Log.RewriteIssued([]), IM.Log.UpdateView, IM.Log.RewriteApplied],
+          log,
+        )
         Assert.equal("an123\n1an23\n12an3\n123an", Editor.Text.getAll(document)->replaceCRLF)
         let log = await IM.insertChar(setup, "d")
         Assert.deepStrictEqual(
diff --git a/test/tests/Test__Give.res b/test/tests/Test__Give.res
index 9294eec8..ca56ae87 100644
--- a/test/tests/Test__Give.res
+++ b/test/tests/Test__Give.res
@@ -9,7 +9,7 @@ describe("agda-mode.give", () => {
   Async.it("should be responded with correct responses", async () => {
     let ctx = await AgdaMode.makeAndLoad("Give.agda")
 
-    let _ = await Editor.Text.insert(ctx.state.document, VSCode.Position.make(7, 14), "y")
+    let _ = await Editor.Text.insert(ctx.state.editor, VSCode.Position.make(7, 14), "y")
     let responses = await ctx.state->State__Connection.sendRequestAndCollectResponses(
       Request.Give({
         index: 0,
diff --git a/test/tests/Test__Goals.res b/test/tests/Test__Goals.res
index b861a227..3db19686 100644
--- a/test/tests/Test__Goals.res
+++ b/test/tests/Test__Goals.res
@@ -32,7 +32,7 @@ describe("Goals", () => {
       "should translate goals on an insertion immediately before a goal",
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
-        let _ = await Editor.Text.insert(ctx.state.document, VSCode.Position.make(8, 18), " ")
+        let _ = await Editor.Text.insert(ctx.state.editor, VSCode.Position.make(8, 18), " ")
         // check the positions of the goals
         Assert.deepStrictEqual(
           Goals.serialize(ctx.state.goals),
@@ -47,7 +47,7 @@ describe("Goals", () => {
       "should translate goals on an insertion immediately after a goal",
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
-        let _ = await Editor.Text.insert(ctx.state.document, VSCode.Position.make(8, 25), " ")
+        let _ = await Editor.Text.insert(ctx.state.editor, VSCode.Position.make(8, 25), " ")
         // check the positions of the goals
         Assert.deepStrictEqual(
           Goals.serialize(ctx.state.goals),
@@ -63,7 +63,7 @@ describe("Goals", () => {
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
         let _ = await Editor.Text.delete(
-          ctx.state.document,
+          ctx.state.editor,
           VSCode.Range.make(VSCode.Position.make(9, 19), VSCode.Position.make(9, 26)),
         )
         // check the positions of the goals
@@ -80,7 +80,7 @@ describe("Goals", () => {
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
         let _ = await Editor.Text.replace(
-          ctx.state.document,
+          ctx.state.editor,
           VSCode.Range.make(VSCode.Position.make(9, 19), VSCode.Position.make(9, 26)),
           "       ",
         )
@@ -98,7 +98,7 @@ describe("Goals", () => {
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
         let _ = await Editor.Text.replace(
-          ctx.state.document,
+          ctx.state.editor,
           VSCode.Range.make(VSCode.Position.make(10, 17), VSCode.Position.make(10, 26)),
           "::DD",
         )
@@ -116,7 +116,7 @@ describe("Goals", () => {
       async () => {
         let ctx = await AgdaMode.makeAndLoad("Goals.agda")
         let _ = await Editor.Text.replace(
-          ctx.state.document,
+          ctx.state.editor,
           VSCode.Range.make(VSCode.Position.make(9, 22), VSCode.Position.make(9, 23)),
           ":D",
         )
@@ -138,7 +138,7 @@ describe("Goals", () => {
           async () => {
             let ctx = await AgdaMode.makeAndLoad("Goals.agda")
             let _ = await Editor.Text.delete(
-              ctx.state.document,
+              ctx.state.editor,
               VSCode.Range.make(VSCode.Position.make(9, 25), VSCode.Position.make(9, 26)),
             )
             await ctx->AgdaMode.quit
@@ -160,7 +160,7 @@ describe("Goals", () => {
           async () => {
             let ctx = await AgdaMode.makeAndLoad("Goals.agda")
             let _ = await Editor.Text.delete(
-              ctx.state.document,
+              ctx.state.editor,
               VSCode.Range.make(VSCode.Position.make(9, 24), VSCode.Position.make(9, 25)),
             )
             await ctx->AgdaMode.quit
@@ -182,7 +182,7 @@ describe("Goals", () => {
           async () => {
             let ctx = await AgdaMode.makeAndLoad("Goals.agda")
             let _ = await Editor.Text.delete(
-              ctx.state.document,
+              ctx.state.editor,
               VSCode.Range.make(VSCode.Position.make(9, 20), VSCode.Position.make(9, 21)),
             )
             await ctx->AgdaMode.quit
@@ -204,7 +204,7 @@ describe("Goals", () => {
           async () => {
             let ctx = await AgdaMode.makeAndLoad("Goals.agda")
             let _ = await Editor.Text.delete(
-              ctx.state.document,
+              ctx.state.editor,
               VSCode.Range.make(VSCode.Position.make(9, 19), VSCode.Position.make(9, 20)),
             )
             await ctx->AgdaMode.quit
diff --git a/test/tests/Test__HelperFunctionType.res b/test/tests/Test__HelperFunctionType.res
index fd6ffb1f..f9de262f 100644
--- a/test/tests/Test__HelperFunctionType.res
+++ b/test/tests/Test__HelperFunctionType.res
@@ -12,7 +12,7 @@ let run = normalization => {
     if versionValid {
       let ctx = await AgdaMode.makeAndLoad(filename)
 
-      let _ = await Editor.Text.insert(ctx.state.document, VSCode.Position.make(7, 14), "y")
+      let _ = await Editor.Text.insert(ctx.state.editor, VSCode.Position.make(7, 14), "y")
       let responses = await ctx.state->State__Connection.sendRequestAndCollectResponses(
         Request.HelperFunctionType(
           normalization,
diff --git a/test/tests/Test__Highlighting.res b/test/tests/Test__Highlighting.res
index 4098c428..221141b2 100644
--- a/test/tests/Test__Highlighting.res
+++ b/test/tests/Test__Highlighting.res
@@ -8,7 +8,7 @@ describe("Highlighting", () => {
 
   Async.it("should work after inserting a newline", async () => {
     let ctx = await AgdaMode.makeAndLoad("Issue180.agda")
-    let _ = await Editor.Text.insert(ctx.state.document, VSCode.Position.make(6, 0), "\n")
+    let _ = await Editor.Text.insert(ctx.state.editor, VSCode.Position.make(6, 0), "\n")
 
     let expected = [
       "(7:0-3) function",
@@ -31,7 +31,7 @@ describe("Highlighting", () => {
     let ctx = await AgdaMode.makeAndLoad("Issue180.agda")
 
     let _ = await Editor.Text.delete(
-      ctx.state.document,
+      ctx.state.editor,
       VSCode.Range.make(VSCode.Position.make(5, 0), VSCode.Position.make(6, 0)),
     )
 
@@ -55,7 +55,7 @@ describe("Highlighting", () => {
     let ctx = await AgdaMode.makeAndLoad("Issue180.agda")
 
     let _ = await Editor.Text.delete(
-      ctx.state.document,
+      ctx.state.editor,
       VSCode.Range.make(VSCode.Position.make(5, 0), VSCode.Position.make(7, 0)),
     )
 
diff --git a/test/tests/Test__UndoRedoHistory.res b/test/tests/Test__UndoRedoHistory.res
new file mode 100644
index 00000000..007b51e4
--- /dev/null
+++ b/test/tests/Test__UndoRedoHistory.res
@@ -0,0 +1,27 @@
+open Mocha
+open Test__Util
+
+@module("vscode") @scope("commands")
+external executeCommand: string => promise<unit> =
+  "executeCommand"
+
+describe_skip("Undo/Redo History", () => {
+  This.timeout(4000)
+  let filename = "CaseSplit.agda"
+  let fileContent = ref("")
+  Async.beforeEach(async () => fileContent := (await File.read(Path.asset(filename))))
+  Async.afterEach(async () => await File.write(Path.asset(filename), fileContent.contents))
+
+  Async.it("shoule make case split a single transaction", async () => {
+    let ctx = await AgdaMode.makeAndLoad(filename)
+    // perform a case split
+    await AgdaMode.case(ctx, ~cursor=VSCode.Position.make(8, 11), ~payload="x")
+    // perform a undo
+    await executeCommand("undo")
+
+    // compare file content before and after
+    let actual = await File.read(Path.asset("CaseSplit.agda"))
+    let expected = fileContent.contents
+    Assert.deepStrictEqual(actual, expected)
+  })
+})
diff --git a/test/tests/Test__Util.res b/test/tests/Test__Util.res
index 249243eb..1a405eb1 100644
--- a/test/tests/Test__Util.res
+++ b/test/tests/Test__Util.res
@@ -21,7 +21,7 @@ module File = {
       VSCode.Position.make(0, 0),
       VSCode.Position.make(lineCount, 0),
     )
-    let succeed = await Editor.Text.replace(document, replaceRange, content)
+    let succeed = await Editor.Text.replace(editor, replaceRange, content)
     if succeed {
       let _ = await VSCode.TextDocument.save(document)
     } else {
@@ -388,7 +388,7 @@ module AgdaMode = {
     let editor = await File.open_(self.filepath)
 
     // set cursor and insert the target for case splitting
-    let succeed = await Editor.Text.insert(self.state.document, cursor, payload)
+    let succeed = await Editor.Text.insert(self.state.editor, cursor, payload)
     if !succeed {
       raise(Failure("Failed to insert text"))
     }
@@ -456,7 +456,7 @@ module AgdaMode = {
       switch payload {
       | None => ()
       | Some(payload) =>
-        let _ = await Editor.Text.insert(self.state.document, cursor, payload)
+        let _ = await Editor.Text.insert(self.state.editor, cursor, payload)
       }
       Editor.Cursor.set(editor, cursor)
     }