diff --git a/lib/js/src/Connection/Emacs/Connection__Emacs.bs.js b/lib/js/src/Connection/Emacs/Connection__Emacs.bs.js
index a2f39e77..b9e9bd05 100644
--- a/lib/js/src/Connection/Emacs/Connection__Emacs.bs.js
+++ b/lib/js/src/Connection/Emacs/Connection__Emacs.bs.js
@@ -4,13 +4,10 @@
 var Os = require("os");
 var Curry = require("rescript/lib/js/curry.js");
 var Nodeos = require("node:os");
-var Js_array = require("rescript/lib/js/js_array.js");
-var Js_string = require("rescript/lib/js/js_string.js");
 var Nodepath = require("node:path");
 var Untildify = require("untildify");
-var Belt_Array = require("rescript/lib/js/belt_Array.js");
-var Belt_Option = require("rescript/lib/js/belt_Option.js");
 var Caml_option = require("rescript/lib/js/caml_option.js");
+var Core__Option = require("@rescript/core/lib/js/src/Core__Option.bs.js");
 var Chan$AgdaModeVscode = require("../../Util/Chan.bs.js");
 var Util$AgdaModeVscode = require("../../Util/Util.bs.js");
 var Config$AgdaModeVscode = require("../../Config.bs.js");
@@ -30,7 +27,7 @@ async function make(path, args) {
     if (hasWeirdPath == null) {
       path$3 = path$2;
     } else {
-      var match$1 = Belt_Array.get(hasWeirdPath, 1);
+      var match$1 = hasWeirdPath[1];
       if (match$1 !== undefined) {
         var drive = Caml_option.valFromOption(match$1);
         if (drive !== undefined) {
@@ -52,15 +49,15 @@ async function make(path, args) {
   var destructor = Client__Process$LanguageServerMule.onOutput($$process, (function (output) {
           switch (output.TAG) {
             case "Stdout" :
-                var match_ = Js_string.match_(/Agda version (.*)/, output._0);
-                if (match_ === undefined) {
+                var match_ = output._0.match(/Agda version (.*)/);
+                if (match_ == null) {
                   return resolve({
                               TAG: "Error",
                               _0: "Cannot read Agda version",
                               [Symbol.for("name")]: "Error"
                             });
                 }
-                var match = Belt_Array.get(match_, 1);
+                var match = match_[1];
                 if (match === undefined) {
                   return resolve({
                               TAG: "Error",
@@ -215,7 +212,7 @@ function wire(self) {
           switch (x.TAG) {
             case "Stdout" :
                 var rawText = x._0;
-                if (Js_string.startsWith("Error:", rawText)) {
+                if (rawText.startsWith("Error:")) {
                   return Chan$AgdaModeVscode.emit(self.chan, {
                               TAG: "Error",
                               _0: {
@@ -226,9 +223,10 @@ function wire(self) {
                               [Symbol.for("name")]: "Error"
                             });
                 } else {
-                  return Belt_Array.forEach(Parser$AgdaModeVscode.splitToLines(rawText), (function (extra) {
-                                return Parser$AgdaModeVscode.Incr.feed(incrParser, extra);
-                              }));
+                  Parser$AgdaModeVscode.splitToLines(rawText).forEach(function (extra) {
+                        return Parser$AgdaModeVscode.Incr.feed(incrParser, extra);
+                      });
+                  return ;
                 }
             case "Stderr" :
                 return Chan$AgdaModeVscode.emit(self.chan, {
@@ -263,7 +261,7 @@ async function make$1(method) {
             [Symbol.for("name")]: "Error"
           };
   }
-  var args = Js_array.concat(Config$AgdaModeVscode.Connection.getCommandLineOptions(), ["--interaction"]);
+  var args = ["--interaction"].concat(Config$AgdaModeVscode.Connection.getCommandLineOptions());
   var e = await make(method._0, args);
   if (e.TAG !== "Ok") {
     return {
@@ -338,7 +336,7 @@ async function onResponse(conn, callback) {
   var listenerHandle;
   listenerHandle = Chan$AgdaModeVscode.on(conn.chan, listener);
   var result = await match[0];
-  Belt_Option.forEach(listenerHandle, (function (destroyListener) {
+  Core__Option.forEach(listenerHandle, (function (destroyListener) {
           destroyListener();
         }));
   return result;
diff --git a/lib/js/src/Parser/Parser.bs.js b/lib/js/src/Parser/Parser.bs.js
index c25f68ed..f82f778b 100644
--- a/lib/js/src/Parser/Parser.bs.js
+++ b/lib/js/src/Parser/Parser.bs.js
@@ -393,21 +393,26 @@ var $$Error = {
   toString: toString$2
 };
 
-function userInputToSExpr(s) {
-  return Js_string.replaceByRe(/\n/g, "\\n", Js_string.replaceByRe(/\r\n/g, "\\r\\n", Js_string.replaceByRe(/\"/g, "\\\"", Js_string.replaceByRe(/\\/g, "\\\\", s)))).trim();
-}
-
 function filepath(s) {
   var removedBidi = Js_string.charCodeAt(0, s) === 8234.0 ? Js_string.sliceToEnd(1, s) : s;
   var normalized = Nodepath.normalize(removedBidi);
   return Js_string.replaceByRe(/\\/g, "/", normalized);
 }
 
+function $$escape(s) {
+  return Js_string.replaceByRe(/\n/g, "\\n", Js_string.replaceByRe(/\r\n/g, "\\r\\n", Js_string.replaceByRe(/\"/g, "\\\"", Js_string.replaceByRe(/\\/g, "\\\\", s)))).trim();
+}
+
+function unescapeEOL(s) {
+  return s.replace(/\\r\\n/g, "\r\n").replace(/\\n/g, "\n");
+}
+
 exports.splitToLines = splitToLines;
 exports.Incr = Incr;
 exports.SExprParseError = SExprParseError;
 exports.SExpression = SExpression;
 exports.$$Error = $$Error;
-exports.userInputToSExpr = userInputToSExpr;
 exports.filepath = filepath;
+exports.$$escape = $$escape;
+exports.unescapeEOL = unescapeEOL;
 /* node:path Not a pure module */
diff --git a/lib/js/src/Request.bs.js b/lib/js/src/Request.bs.js
index 0febfb7b..0dffe777 100644
--- a/lib/js/src/Request.bs.js
+++ b/lib/js/src/Request.bs.js
@@ -140,12 +140,12 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
           }
       case "SearchAbout" :
           var normalization$3 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_search_about_toplevel " + normalization$3 + " \"" + content + "\" )";
       case "Give" :
           var goal = request._0;
           var index$1 = String(goal.index);
-          var content$1 = Parser$AgdaModeVscode.userInputToSExpr(Goal$AgdaModeVscode.getContent(goal, $$document));
+          var content$1 = Parser$AgdaModeVscode.$$escape(Goal$AgdaModeVscode.getContent(goal, $$document));
           var range = buildRange(goal);
           if (Util$AgdaModeVscode.Version.gte(version, "2.5.3")) {
             return commonPart("NonInteractive") + "( Cmd_give WithoutForce " + index$1 + " " + range + " \"" + content$1 + "\" )";
@@ -155,19 +155,19 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
       case "Refine" :
           var goal$1 = request._0;
           var index$2 = String(goal$1.index);
-          var content$2 = Parser$AgdaModeVscode.userInputToSExpr(Goal$AgdaModeVscode.getContent(goal$1, $$document));
+          var content$2 = Parser$AgdaModeVscode.$$escape(Goal$AgdaModeVscode.getContent(goal$1, $$document));
           var range$1 = buildRange(goal$1);
           return commonPart("NonInteractive") + "( Cmd_refine_or_intro False " + index$2 + " " + range$1 + " \"" + content$2 + "\" )";
       case "ElaborateAndGive" :
           var index$3 = String(request._2.index);
           var normalization$4 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$3 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$3 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_elaborate_give " + normalization$4 + " " + index$3 + " noRange \"" + content$3 + "\" )";
       case "Auto" :
           var goal$2 = request._1;
           var normalization$5 = Command$AgdaModeVscode.Normalization.encode(request._0);
           var index$4 = String(goal$2.index);
-          var content$4 = Parser$AgdaModeVscode.userInputToSExpr(Goal$AgdaModeVscode.getContent(goal$2, $$document));
+          var content$4 = Parser$AgdaModeVscode.$$escape(Goal$AgdaModeVscode.getContent(goal$2, $$document));
           var range$2 = buildRange(goal$2);
           if (Util$AgdaModeVscode.Version.gte(version, "2.7.0")) {
             return commonPart("NonInteractive") + "( Cmd_autoOne " + normalization$5 + " " + index$4 + " " + range$2 + " \"" + content$4 + "\" )";
@@ -179,22 +179,22 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
       case "Case" :
           var goal$3 = request._0;
           var index$5 = String(goal$3.index);
-          var content$5 = Parser$AgdaModeVscode.userInputToSExpr(Goal$AgdaModeVscode.getContent(goal$3, $$document));
+          var content$5 = Parser$AgdaModeVscode.$$escape(Goal$AgdaModeVscode.getContent(goal$3, $$document));
           var range$3 = buildRange(goal$3);
           return commonPart("NonInteractive") + "( Cmd_make_case " + index$5 + " " + range$3 + " \"" + content$5 + "\" )";
       case "HelperFunctionType" :
           var index$6 = String(request._2.index);
           var normalization$6 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$6 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$6 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_helper_function " + normalization$6 + " " + index$6 + " noRange \"" + content$6 + "\" )";
       case "InferType" :
           var index$7 = String(request._2.index);
           var normalization$7 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$7 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$7 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_infer " + normalization$7 + " " + index$7 + " noRange \"" + content$7 + "\" )";
       case "InferTypeGlobal" :
           var normalization$8 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$8 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$8 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("None") + "( Cmd_infer_toplevel " + normalization$8 + " \"" + content$8 + "\" )";
       case "Context" :
           var index$8 = String(request._1.index);
@@ -211,28 +211,28 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
       case "GoalTypeContextAndInferredType" :
           var index$11 = String(request._2.index);
           var normalization$12 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$9 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$9 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_goal_type_context_infer " + normalization$12 + " " + index$11 + " noRange \"" + content$9 + "\" )";
       case "GoalTypeContextAndCheckedType" :
           var index$12 = String(request._2.index);
           var normalization$13 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$10 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$10 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_goal_type_context_check " + normalization$13 + " " + index$12 + " noRange \"" + content$10 + "\" )";
       case "ModuleContents" :
           var index$13 = String(request._2.index);
           var normalization$14 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$11 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$11 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("NonInteractive") + "( Cmd_show_module_contents " + normalization$14 + " " + index$13 + " noRange \"" + content$11 + "\" )";
       case "ModuleContentsGlobal" :
           var normalization$15 = Command$AgdaModeVscode.Normalization.encode(request._0);
-          var content$12 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$12 = Parser$AgdaModeVscode.$$escape(request._1);
           return commonPart("None") + "( Cmd_show_module_contents_toplevel " + normalization$15 + " \"" + content$12 + "\" )";
       case "ComputeNormalForm" :
           var computeMode = request._0;
           var index$14 = String(request._2.index);
           var ignoreAbstract = PervasivesU.string_of_bool(Command$AgdaModeVscode.ComputeMode.ignoreAbstract(computeMode));
           var computeMode$1 = Command$AgdaModeVscode.ComputeMode.encode(computeMode);
-          var content$13 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$13 = Parser$AgdaModeVscode.$$escape(request._1);
           if (Util$AgdaModeVscode.Version.gte(version, "2.5.2")) {
             return commonPart("NonInteractive") + "( Cmd_compute " + computeMode$1 + " " + index$14 + " noRange \"" + content$13 + "\" )";
           } else {
@@ -242,7 +242,7 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
           var computeMode$2 = request._0;
           var ignoreAbstract$1 = PervasivesU.string_of_bool(Command$AgdaModeVscode.ComputeMode.ignoreAbstract(computeMode$2));
           var computeMode$3 = Command$AgdaModeVscode.ComputeMode.encode(computeMode$2);
-          var content$14 = Parser$AgdaModeVscode.userInputToSExpr(request._1);
+          var content$14 = Parser$AgdaModeVscode.$$escape(request._1);
           if (Util$AgdaModeVscode.Version.gte(version, "2.5.2")) {
             return commonPart("NonInteractive") + "( Cmd_compute_toplevel " + computeMode$3 + " \"" + content$14 + "\" )";
           } else {
@@ -250,10 +250,10 @@ function encode($$document, version, filepath, backend, libraryPath, highlightin
           }
       case "WhyInScope" :
           var index$15 = String(request._1.index);
-          var content$15 = Parser$AgdaModeVscode.userInputToSExpr(request._0);
+          var content$15 = Parser$AgdaModeVscode.$$escape(request._0);
           return commonPart("NonInteractive") + "( Cmd_why_in_scope " + index$15 + " noRange \"" + content$15 + "\" )";
       case "WhyInScopeGlobal" :
-          var content$16 = Parser$AgdaModeVscode.userInputToSExpr(request._0);
+          var content$16 = Parser$AgdaModeVscode.$$escape(request._0);
           return commonPart("None") + "( Cmd_why_in_scope_toplevel \"" + content$16 + "\" )";
       
     }
diff --git a/lib/js/src/Response.bs.js b/lib/js/src/Response.bs.js
index 544c2153..e6bc649c 100644
--- a/lib/js/src/Response.bs.js
+++ b/lib/js/src/Response.bs.js
@@ -113,7 +113,7 @@ function parse(xs) {
   if (match.TAG !== "A") {
     return ;
   }
-  var payload = match._0.replace(/\\n|\\r\\n/g, "\n");
+  var payload = Parser$AgdaModeVscode.unescapeEOL(match._0);
   var match$1 = xs[0];
   if (match$1 === undefined) {
     return ;
@@ -777,7 +777,7 @@ function parse$1(tokens) {
                   _0: {
                     TAG: "RunningInfo",
                     _0: 2,
-                    _1: match$7._0,
+                    _1: Parser$AgdaModeVscode.unescapeEOL(match$7._0),
                     [Symbol.for("name")]: "RunningInfo"
                   },
                   [Symbol.for("name")]: "Ok"
@@ -840,7 +840,7 @@ function parse$1(tokens) {
                   _0: {
                     TAG: "RunningInfo",
                     _0: 1,
-                    _1: match$10._0,
+                    _1: Parser$AgdaModeVscode.unescapeEOL(match$10._0),
                     [Symbol.for("name")]: "RunningInfo"
                   },
                   [Symbol.for("name")]: "Ok"
diff --git a/lib/js/src/State/State__Goal.bs.js b/lib/js/src/State/State__Goal.bs.js
index 02d29ac1..86b9ad9f 100644
--- a/lib/js/src/State/State__Goal.bs.js
+++ b/lib/js/src/State/State__Goal.bs.js
@@ -330,6 +330,7 @@ var Module = {
   pointed: pointed,
   replaceWithLines: replaceWithLines,
   replaceWithLambda: replaceWithLambda,
+  indentationWidth: indentationWidth,
   caseSplitAux: caseSplitAux,
   redecorate: redecorate,
   next: next,
@@ -343,6 +344,7 @@ exports.removeBoundaryAndDestroy = removeBoundaryAndDestroy;
 exports.pointed = pointed;
 exports.replaceWithLines = replaceWithLines;
 exports.replaceWithLambda = replaceWithLambda;
+exports.indentationWidth = indentationWidth;
 exports.caseSplitAux = caseSplitAux;
 exports.redecorate = redecorate;
 exports.next = next;
diff --git a/lib/js/src/State/State__Response.bs.js b/lib/js/src/State/State__Response.bs.js
index 32cf3b5a..6d7399f5 100644
--- a/lib/js/src/State/State__Response.bs.js
+++ b/lib/js/src/State/State__Response.bs.js
@@ -2,7 +2,6 @@
 'use strict';
 
 var Vscode = require("vscode");
-var Js_string = require("rescript/lib/js/js_string.js");
 var Chan$AgdaModeVscode = require("../Util/Chan.bs.js");
 var Item$AgdaModeVscode = require("../View/Component/Item.bs.js");
 var Util$AgdaModeVscode = require("../Util/Util.bs.js");
@@ -16,8 +15,9 @@ var State__View$AgdaModeVscode = require("./State__View.bs.js");
 var Highlighting$AgdaModeVscode = require("../Highlighting.bs.js");
 var Emacs__Parser2$AgdaModeVscode = require("../View/Panel/Emacs/Emacs__Parser2.bs.js");
 
-function removeNewlines(string) {
-  return string.split("\n").join("\n");
+function indent(content, indent$1) {
+  var indentation = " ".repeat(indent$1);
+  return content.replace(/\n/g, "\n" + indentation);
 }
 
 async function handle(state, x) {
@@ -276,18 +276,20 @@ async function handle$1(state, dispatchCommand, response) {
               return await State__Goal$AgdaModeVscode.removeBoundaryAndDestroy(state, goal);
             } else {
               var content = give._0;
+              var match = State__Goal$AgdaModeVscode.indentationWidth(state.document, goal);
+              var indentationWidth = match[0];
               await State__Goal$AgdaModeVscode.modify(state, goal, (function (param) {
-                      return Js_string.replaceByRe(/\\\\n/g, "\n", content);
+                      return indent(Parser$AgdaModeVscode.unescapeEOL(content), 2 + indentationWidth | 0);
                     }));
               return await State__Goal$AgdaModeVscode.removeBoundaryAndDestroy(state, goal);
             }
         case "MakeCase" :
             var lines = response._1;
-            var match = State__Goal$AgdaModeVscode.pointed(state);
-            if (match === undefined) {
+            var match$1 = State__Goal$AgdaModeVscode.pointed(state);
+            if (match$1 === undefined) {
               return await State__View$AgdaModeVscode.Panel.displayOutOfGoalError(state);
             }
-            var goal$1 = match[0];
+            var goal$1 = match$1[0];
             if (response._0 === "Function") {
               await State__Goal$AgdaModeVscode.replaceWithLines(state, goal$1, lines);
             } else {
@@ -335,23 +337,22 @@ async function handle$1(state, dispatchCommand, response) {
             return await handle(state, response._0);
         case "RunningInfo" :
             var verbosity = response._0;
-            if (verbosity !== 1) {
-              var message = removeNewlines(response._1);
-              state.runningInfoLog.push([
-                    verbosity,
-                    message
-                  ]);
-              return await State__View$AgdaModeVscode.DebugBuffer.displayInAppendMode([[
-                            verbosity,
-                            message
-                          ]]);
+            if (verbosity === 1) {
+              return await State__View$AgdaModeVscode.Panel.displayInAppendMode(state, {
+                          TAG: "Plain",
+                          _0: "Type-checking",
+                          [Symbol.for("name")]: "Plain"
+                        }, [Item$AgdaModeVscode.plainText(response._1)]);
             }
-            var message$1 = removeNewlines(response._1);
-            return await State__View$AgdaModeVscode.Panel.displayInAppendMode(state, {
-                        TAG: "Plain",
-                        _0: "Type-checking",
-                        [Symbol.for("name")]: "Plain"
-                      }, [Item$AgdaModeVscode.plainText(message$1)]);
+            var message = response._1;
+            state.runningInfoLog.push([
+                  verbosity,
+                  message
+                ]);
+            return await State__View$AgdaModeVscode.DebugBuffer.displayInAppendMode([[
+                          verbosity,
+                          message
+                        ]]);
         
       }
     }
@@ -360,7 +361,7 @@ async function handle$1(state, dispatchCommand, response) {
   return Chan$AgdaModeVscode.emit(state.channels.responseHandled, response);
 }
 
-exports.removeNewlines = removeNewlines;
+exports.indent = indent;
 exports.DisplayInfo = DisplayInfo;
 exports.handle = handle$1;
 /* vscode Not a pure module */
diff --git a/lib/js/test/tests/Parser/Test__Parser.bs.js b/lib/js/test/tests/Parser/Test__Parser.bs.js
index dad983f0..0d525deb 100644
--- a/lib/js/test/tests/Parser/Test__Parser.bs.js
+++ b/lib/js/test/tests/Parser/Test__Parser.bs.js
@@ -5,23 +5,34 @@ var Curry = require("rescript/lib/js/curry.js");
 var Assert = require("assert");
 var Parser$AgdaModeVscode = require("../../../src/Parser/Parser.bs.js");
 
-describe("when running Parser.userInputToSExpr", (function () {
+describe("when running Parser.escape", (function () {
         it("should make escaped backslash explicit", (function () {
-                var actual = Parser$AgdaModeVscode.userInputToSExpr("\\ x -> x");
+                var actual = Parser$AgdaModeVscode.$$escape("\\ x -> x");
                 Curry._3(Assert.deepEqual, actual, "\\\\ x -> x", undefined);
               }));
         it("should make escaped newline on Unix explicit", (function () {
-                var actual = Parser$AgdaModeVscode.userInputToSExpr("x\ny");
+                var actual = Parser$AgdaModeVscode.$$escape("x\ny");
                 Curry._3(Assert.deepEqual, actual, "x\\ny", undefined);
               }));
         it("should make escaped newline on Windows explicit", (function () {
-                var actual = Parser$AgdaModeVscode.userInputToSExpr("x\r\ny");
+                var actual = Parser$AgdaModeVscode.$$escape("x\r\ny");
                 Curry._3(Assert.deepEqual, actual, "x\\r\\ny", undefined);
               }));
         it("should make escaped double quote explicit", (function () {
-                var actual = Parser$AgdaModeVscode.userInputToSExpr("\"x\"");
+                var actual = Parser$AgdaModeVscode.$$escape("\"x\"");
                 Curry._3(Assert.deepEqual, actual, "\\\"x\\\"", undefined);
               }));
       }));
 
+describe("when running Parser.unescapeEOL", (function () {
+        it("should make explicit newline on Unix implicit", (function () {
+                var actual = Parser$AgdaModeVscode.unescapeEOL("x\\ny");
+                Curry._3(Assert.deepEqual, actual, "x\ny", undefined);
+              }));
+        it("should make explicit newline on Windows implicit", (function () {
+                var actual = Parser$AgdaModeVscode.unescapeEOL("x\\r\\ny");
+                Curry._3(Assert.deepEqual, actual, "x\r\ny", undefined);
+              }));
+      }));
+
 /*  Not a pure module */
diff --git a/lib/js/test/tests/Test__Auto.bs.js b/lib/js/test/tests/Test__Auto.bs.js
index 9279ac66..33c5ed16 100644
--- a/lib/js/test/tests/Test__Auto.bs.js
+++ b/lib/js/test/tests/Test__Auto.bs.js
@@ -11,17 +11,16 @@ function run(normalization) {
   describe("request to Agda", (function () {
           describe("global", (function () {
                   it("should be responded with the correct answer 1", (async function () {
-                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "Auto.agda");
-                          var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
+                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "Auto.agda");
                           var responses = {
                             contents: []
                           };
                           var responseHandler = async function (response) {
                             responses.contents.push(response);
                           };
-                          var goal = state.goals[0];
+                          var goal = ctx.state.goals[0];
                           if (goal !== undefined) {
-                            await State$AgdaModeVscode.sendRequest(state, responseHandler, {
+                            await State$AgdaModeVscode.sendRequest(ctx.state, responseHandler, {
                                   TAG: "Auto",
                                   _0: normalization,
                                   _1: goal,
@@ -30,7 +29,7 @@ function run(normalization) {
                           } else {
                             Assert.fail("No goals found");
                           }
-                          var version = state.agdaVersion;
+                          var version = ctx.state.agdaVersion;
                           if (version !== undefined) {
                             if (Util$AgdaModeVscode.Version.gte(version, "2.7.0")) {
                               return Curry._3(Assert.deepEqual, responses.contents, [
@@ -93,17 +92,16 @@ function run(normalization) {
                           }
                         }));
                   it("should be responded with the correct answer 2", (async function () {
-                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "Auto.agda");
-                          var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
+                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "Auto.agda");
                           var responses = {
                             contents: []
                           };
                           var responseHandler = async function (response) {
                             responses.contents.push(response);
                           };
-                          var goal = state.goals[1];
+                          var goal = ctx.state.goals[1];
                           if (goal !== undefined) {
-                            await State$AgdaModeVscode.sendRequest(state, responseHandler, {
+                            await State$AgdaModeVscode.sendRequest(ctx.state, responseHandler, {
                                   TAG: "Auto",
                                   _0: normalization,
                                   _1: goal,
@@ -112,7 +110,7 @@ function run(normalization) {
                           } else {
                             Assert.fail("No goals found");
                           }
-                          var version = state.agdaVersion;
+                          var version = ctx.state.agdaVersion;
                           if (version !== undefined) {
                             if (Util$AgdaModeVscode.Version.gte(version, "2.7.0")) {
                               return Curry._3(Assert.deepEqual, responses.contents, [
diff --git a/lib/js/test/tests/Test__CaseSplit.bs.js b/lib/js/test/tests/Test__CaseSplit.bs.js
index 51b99304..499068c1 100644
--- a/lib/js/test/tests/Test__CaseSplit.bs.js
+++ b/lib/js/test/tests/Test__CaseSplit.bs.js
@@ -89,20 +89,19 @@ describe("agda-mode:case", (function () {
         var fileContent = {
           contents: ""
         };
-        before(function () {
-              return Test__Util$AgdaModeVscode.readFile(Test__Util$AgdaModeVscode.Path.asset("CaseSplit.agda"), fileContent);
+        before(async function () {
+              fileContent.contents = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset("CaseSplit.agda"));
             });
-        after(function () {
-              return Test__Util$AgdaModeVscode.restoreFile(Test__Util$AgdaModeVscode.Path.asset("CaseSplit.agda"), fileContent);
+        after(async function () {
+              return await Test__Util$AgdaModeVscode.$$File.write(Test__Util$AgdaModeVscode.Path.asset("CaseSplit.agda"), fileContent.contents);
             });
         it("should have more goals after splitting", (async function () {
-                var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "CaseSplit.agda");
-                var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
-                var state$1 = await Test__Util$AgdaModeVscode.AgdaMode.$$case(ctx, [
+                var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "CaseSplit.agda");
+                await Test__Util$AgdaModeVscode.AgdaMode.$$case(ctx, [
                       new Vscode.Position(7, 16),
                       "x"
-                    ], state);
-                return Curry._3(Assert.deepEqual, state$1.goals.length, 10, undefined);
+                    ]);
+                return Curry._3(Assert.deepEqual, ctx.state.goals.length, 10, undefined);
               }));
       }));
 
diff --git a/lib/js/test/tests/Test__ComputeNormalForm.bs.js b/lib/js/test/tests/Test__ComputeNormalForm.bs.js
index b10a1001..e1ad9ecd 100644
--- a/lib/js/test/tests/Test__ComputeNormalForm.bs.js
+++ b/lib/js/test/tests/Test__ComputeNormalForm.bs.js
@@ -10,15 +10,14 @@ function run(normalization) {
   describe("request to Agda", (function () {
           describe("global", (function () {
                   it("should be responded with the correct answer", (async function () {
-                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "ComputeNormalForm.agda");
-                          var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
+                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "ComputeNormalForm.agda");
                           var responses = {
                             contents: []
                           };
                           var responseHandler = async function (response) {
                             responses.contents.push(response);
                           };
-                          await State$AgdaModeVscode.sendRequest(state, responseHandler, {
+                          await State$AgdaModeVscode.sendRequest(ctx.state, responseHandler, {
                                 TAG: "ComputeNormalFormGlobal",
                                 _0: normalization,
                                 _1: "Z + S Z",
@@ -44,15 +43,14 @@ function run(normalization) {
                                     ], undefined);
                         }));
                   it("should be responded with the correct answer", (async function () {
-                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "ComputeNormalForm.agda");
-                          var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
+                          var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "ComputeNormalForm.agda");
                           var responses = {
                             contents: []
                           };
                           var responseHandler = async function (response) {
                             responses.contents.push(response);
                           };
-                          await State$AgdaModeVscode.sendRequest(state, responseHandler, {
+                          await State$AgdaModeVscode.sendRequest(ctx.state, responseHandler, {
                                 TAG: "ComputeNormalFormGlobal",
                                 _0: normalization,
                                 _1: "S Z + S Z",
diff --git a/lib/js/test/tests/Test__Refine.bs.js b/lib/js/test/tests/Test__Refine.bs.js
new file mode 100644
index 00000000..d5a76cf2
--- /dev/null
+++ b/lib/js/test/tests/Test__Refine.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 Caml_option = require("rescript/lib/js/caml_option.js");
+var Test__Util$AgdaModeVscode = require("./Test__Util.bs.js");
+
+describe("agda-mode.refine", (function () {
+        describe("Issue #158", (function () {
+                var fileContent = {
+                  contents: ""
+                };
+                before(async function () {
+                      fileContent.contents = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset("Issue158.agda"));
+                    });
+                after(async function () {
+                      return await Test__Util$AgdaModeVscode.$$File.write(Test__Util$AgdaModeVscode.Path.asset("Issue158.agda"), fileContent.contents);
+                    });
+                it("should be result in the correct refinement", (async function () {
+                        var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "Issue158.agda");
+                        await Test__Util$AgdaModeVscode.AgdaMode.refine(ctx, Caml_option.some(new Vscode.Position(12, 9)), undefined);
+                        var actual = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset("Issue158.agda"));
+                        var expected = await Test__Util$AgdaModeVscode.$$File.read(Test__Util$AgdaModeVscode.Path.asset("Issue158.agda.out"));
+                        return Curry._3(Assert.equal, actual, expected, undefined);
+                      }));
+              }));
+      }));
+
+/*  Not a pure module */
diff --git a/lib/js/test/tests/Test__Tokens.bs.js b/lib/js/test/tests/Test__Tokens.bs.js
index efbe9ae3..79d6ce3e 100644
--- a/lib/js/test/tests/Test__Tokens.bs.js
+++ b/lib/js/test/tests/Test__Tokens.bs.js
@@ -11,17 +11,15 @@ describe("Tokens", (function () {
         this.timeout(10000);
         describe("GotoDefinition.agda", (function () {
                 it("should produce 28 tokens", (async function () {
-                        var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "GotoDefinition.agda");
-                        var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
-                        var tokens = Tokens$AgdaModeVscode.toArray(state.tokens).map(function (param) {
+                        var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "GotoDefinition.agda");
+                        var tokens = Tokens$AgdaModeVscode.toArray(ctx.state.tokens).map(function (param) {
                               return Editor$AgdaModeVscode.$$Range.toString(param[1]) + " " + Tokens$AgdaModeVscode.Token.toString(param[0]);
                             });
                         return Curry._3(Assert.deepEqual, 28, tokens.length, undefined);
                       }));
                 it("should produce correct tokens", (async function () {
-                        var ctx = await Test__Util$AgdaModeVscode.AgdaMode.make(undefined, "GotoDefinition.agda");
-                        var state = await Test__Util$AgdaModeVscode.AgdaMode.load(ctx);
-                        var tokens = Tokens$AgdaModeVscode.toArray(state.tokens).map(function (param) {
+                        var ctx = await Test__Util$AgdaModeVscode.AgdaMode.makeAndLoad(undefined, "GotoDefinition.agda");
+                        var tokens = Tokens$AgdaModeVscode.toArray(ctx.state.tokens).map(function (param) {
                               return Editor$AgdaModeVscode.$$Range.toString(param[1]) + " " + Tokens$AgdaModeVscode.Token.toString(param[0]);
                             });
                         return Curry._3(Assert.deepEqual, [
diff --git a/lib/js/test/tests/Test__Util.bs.js b/lib/js/test/tests/Test__Util.bs.js
index 5058a2a6..2ec1cf79 100644
--- a/lib/js/test/tests/Test__Util.bs.js
+++ b/lib/js/test/tests/Test__Util.bs.js
@@ -13,6 +13,7 @@ var Js_array = require("rescript/lib/js/js_array.js");
 var Js_string = require("rescript/lib/js/js_string.js");
 var Nodepath = require("node:path");
 var Js_promise = require("rescript/lib/js/js_promise.js");
+var Caml_option = require("rescript/lib/js/caml_option.js");
 var Core__Option = require("@rescript/core/lib/js/src/Core__Option.bs.js");
 var Caml_exceptions = require("rescript/lib/js/caml_exceptions.js");
 var Chan$AgdaModeVscode = require("../../src/Util/Chan.bs.js");
@@ -27,6 +28,39 @@ var Connection__Emacs__Error$AgdaModeVscode = require("../../src/Connection/Emac
 
 var Exn = /* @__PURE__ */Caml_exceptions.create("Test__Util-AgdaModeVscode.Exn");
 
+function open_(fileName) {
+  return Vscode.window.showTextDocument(Vscode.Uri.file(fileName), undefined);
+}
+
+async function read(fileName) {
+  var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(fileName), undefined);
+  var $$document = editor.document;
+  return $$document.getText(undefined);
+}
+
+async function write(fileName, content) {
+  var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(fileName), undefined);
+  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);
+  if (succeed) {
+    await $$document.save();
+    return ;
+  }
+  throw {
+        RE_EXN_ID: "Failure",
+        _1: "Failed to write to " + fileName,
+        Error: new Error()
+      };
+}
+
+var $$File = {
+  open_: open_,
+  read: read,
+  write: write
+};
+
 var runner = (function(f) {
     var tmp
     try {
@@ -82,10 +116,6 @@ function activateExtension() {
   return channels$1;
 }
 
-function openFile(fileName) {
-  return Vscode.window.showTextDocument(Vscode.Uri.file(fileName), undefined);
-}
-
 async function activateExtensionAndOpenFile(fileName) {
   var channels = activateExtension();
   var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(fileName), undefined);
@@ -339,55 +369,57 @@ async function exists(command) {
       };
 }
 
-async function make(alsOpt, filepath) {
+async function makeAndLoad(alsOpt, filepath) {
   var als = alsOpt !== undefined ? alsOpt : false;
   var filepath$1 = asset(filepath);
   Config$AgdaModeVscode.inTestingMode.contents = true;
   await Config$AgdaModeVscode.Connection.setAgdaVersion("agda");
   await Config$AgdaModeVscode.Connection.setUseAgdaLanguageServer(als);
   await exists("agda");
-  return {
-          filepath: filepath$1,
-          channels: activateExtension()
-        };
-}
-
-async function load(self) {
-  var match = Util$AgdaModeVscode.Promise_.pending();
-  var resolve = match[1];
-  var disposable = Chan$AgdaModeVscode.on(self.channels.responseHandled, (function (response) {
-          if (typeof response !== "object" && response === "CompleteHighlightingAndMakePromptReappear") {
-            return resolve();
-          }
-          
-        }));
-  await Vscode.window.showTextDocument(Vscode.Uri.file(self.filepath), undefined);
-  var match$1 = await Vscode.commands.executeCommand("agda-mode.load");
-  if (match$1 !== undefined) {
-    if (match$1.TAG === "Ok") {
-      await match[0];
-      disposable();
-      return match$1._0;
+  var load = async function (channels, filepath) {
+    var match = Util$AgdaModeVscode.Promise_.pending();
+    var resolve = match[1];
+    var disposable = Chan$AgdaModeVscode.on(channels.responseHandled, (function (response) {
+            if (typeof response !== "object" && response === "CompleteHighlightingAndMakePromptReappear") {
+              return resolve();
+            }
+            
+          }));
+    await Vscode.window.showTextDocument(Vscode.Uri.file(filepath), undefined);
+    var match$1 = await Vscode.commands.executeCommand("agda-mode.load");
+    if (match$1 !== undefined) {
+      if (match$1.TAG === "Ok") {
+        await match[0];
+        disposable();
+        return match$1._0;
+      }
+      var match$2 = Connection__Error$AgdaModeVscode.toString(match$1._0);
+      throw {
+            RE_EXN_ID: "Failure",
+            _1: match$2[0] + "\n" + match$2[1],
+            Error: new Error()
+          };
     }
-    var match$2 = Connection__Error$AgdaModeVscode.toString(match$1._0);
     throw {
           RE_EXN_ID: "Failure",
-          _1: match$2[0] + "\n" + match$2[1],
+          _1: "Cannot load " + filepath,
           Error: new Error()
         };
-  }
-  throw {
-        RE_EXN_ID: "Failure",
-        _1: "Cannot load " + self.filepath,
-        Error: new Error()
-      };
+  };
+  var channels = activateExtension();
+  var state = await load(channels, filepath$1);
+  return {
+          filepath: filepath$1,
+          channels: channels,
+          state: state
+        };
 }
 
-async function $$case(self, cursorAndPayload, state) {
+async function $$case(self, cursorAndPayload) {
   var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(self.filepath), undefined);
   if (cursorAndPayload !== undefined) {
     var cursor = cursorAndPayload[0];
-    var succeed = await Editor$AgdaModeVscode.$$Text.insert(state.document, cursor, cursorAndPayload[1]);
+    var succeed = await Editor$AgdaModeVscode.$$Text.insert(self.state.document, cursor, cursorAndPayload[1]);
     if (!succeed) {
       throw {
             RE_EXN_ID: "Failure",
@@ -399,7 +431,7 @@ async function $$case(self, cursorAndPayload, state) {
   }
   var match = Util$AgdaModeVscode.Promise_.pending();
   var resolve = match[1];
-  var destructor = Chan$AgdaModeVscode.on(state.channels.commandHandled, (function (command) {
+  var destructor = Chan$AgdaModeVscode.on(self.state.channels.commandHandled, (function (command) {
           if (typeof command !== "object" && command === "Load") {
             return resolve();
           }
@@ -410,7 +442,8 @@ async function $$case(self, cursorAndPayload, state) {
     if (match$1.TAG === "Ok") {
       await match[0];
       destructor();
-      return match$1._0;
+      self.state = match$1._0;
+      return ;
     }
     var match$2 = Connection__Error$AgdaModeVscode.toString(match$1._0);
     throw {
@@ -426,22 +459,20 @@ async function $$case(self, cursorAndPayload, state) {
       };
 }
 
-async function refine(self, cursorAndPayload, state) {
+async function refine(self, cursor, payload) {
   var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(self.filepath), undefined);
-  if (cursorAndPayload !== undefined) {
-    var payload = cursorAndPayload[1];
-    var cursor = cursorAndPayload[0];
+  if (cursor !== undefined) {
+    var cursor$1 = Caml_option.valFromOption(cursor);
     if (payload !== undefined) {
-      await Editor$AgdaModeVscode.$$Text.insert(state.document, cursor, payload);
-      Editor$AgdaModeVscode.Cursor.set(editor, cursor);
-    } else {
-      Editor$AgdaModeVscode.Cursor.set(editor, cursor);
+      await Editor$AgdaModeVscode.$$Text.insert(self.state.document, cursor$1, payload);
     }
+    Editor$AgdaModeVscode.Cursor.set(editor, cursor$1);
   }
   var match = await Vscode.commands.executeCommand("agda-mode.refine");
   if (match !== undefined) {
     if (match.TAG === "Ok") {
-      return match._0;
+      self.state = match._0;
+      return ;
     }
     var match$1 = Connection__Error$AgdaModeVscode.toString(match._0);
     throw {
@@ -460,68 +491,21 @@ async function refine(self, cursorAndPayload, state) {
 var AgdaMode = {
   $$Error: $$Error,
   exists: exists,
-  make: make,
-  load: load,
+  makeAndLoad: makeAndLoad,
   $$case: $$case,
   refine: refine
 };
 
-async function readFile$1(filepath, $$var) {
-  var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(filepath), undefined);
-  $$var.contents = Editor$AgdaModeVscode.$$Text.getAll(editor.document);
-}
-
-async function restoreFile(filepath, $$var) {
-  var editor = await Vscode.window.showTextDocument(Vscode.Uri.file(filepath), undefined);
-  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, $$var.contents);
-  if (succeed) {
-    await $$document.save();
-    return ;
-  }
-  throw {
-        RE_EXN_ID: "Failure",
-        _1: "Failed to restore the file",
-        Error: new Error()
-      };
-}
-
-function unwrap(x) {
-  if (x.TAG === "Ok") {
-    return x._0;
-  }
-  throw x._0;
-}
-
-var R = {
-  unwrap: unwrap
-};
-
-async function unwrap$1(promise) {
-  var result = await promise;
-  return unwrap(result);
-}
-
-var P = {
-  unwrap: unwrap$1
-};
-
 exports.Exn = Exn;
+exports.$$File = $$File;
 exports.runner = runner;
 exports.Path = Path;
 exports.activationSingleton = activationSingleton;
 exports.activateExtension = activateExtension;
-exports.openFile = openFile;
 exports.activateExtensionAndOpenFile = activateExtensionAndOpenFile;
 exports.wait = wait;
 exports.Strings = Strings;
 exports.Golden = Golden;
 exports.onUnix = onUnix;
 exports.AgdaMode = AgdaMode;
-exports.readFile = readFile$1;
-exports.restoreFile = restoreFile;
-exports.R = R;
-exports.P = P;
 /* extensionPath Not a pure module */
diff --git a/src/Connection/Connection.res b/src/Connection/Connection.res
index be8b591c..5f1e5a1e 100644
--- a/src/Connection/Connection.res
+++ b/src/Connection/Connection.res
@@ -162,7 +162,8 @@ module Module: Module = {
     | None =>
       switch await start(globalStoragePath, useLSP, onDownload) {
       | Error(error) => Error(error)
-      | Ok(_) => await sendRequest(globalStoragePath, onDownload, useLSP, document, request, handler)
+      | Ok(_) =>
+        await sendRequest(globalStoragePath, onDownload, useLSP, document, request, handler)
       }
     }
   }
diff --git a/src/Connection/Emacs/Connection__Emacs.res b/src/Connection/Emacs/Connection__Emacs.res
index 98f907b4..2b32d52c 100644
--- a/src/Connection/Emacs/Connection__Emacs.res
+++ b/src/Connection/Emacs/Connection__Emacs.res
@@ -1,5 +1,3 @@
-open Belt
-
 module Error = Connection__Emacs__Error
 module Scheduler = Connection__Scheduler
 module Process = LanguageServerMule.Client.Process
@@ -51,7 +49,7 @@ module ProcInfo: {
     let destructor = process->Process.onOutput(output =>
       switch output {
       | Process.Stdout(output) =>
-        switch Js.String.match_(%re("/Agda version (.*)/"), output) {
+        switch String.match(output, %re("/Agda version (.*)/")) {
         | None => resolve(Error("Cannot read Agda version"))
         | Some(match_) =>
           switch match_[1] {
@@ -173,7 +171,7 @@ module Module: Module = {
         switch x {
         | Stdout(rawText) =>
           // sometimes Agda would return error messages from STDOUT
-          if Js.String.startsWith("Error:", rawText) {
+          if rawText->String.startsWith("Error:") {
             self.chan->Chan.emit(Error(AgdaError(rawText)))
           } else {
             // split the raw text into pieces and feed it to the parser
@@ -191,9 +189,7 @@ module Module: Module = {
     switch method {
     | LanguageServerMule.Method.ViaTCP(_) => Error(Error.ConnectionViaTCPNotSupported)
     | ViaPipe(path, _, _, _) =>
-      // Js.Array.concat([1, 2, 3], [4, 5, 6]) == [4, 5, 6, 1, 2, 3], fuck me right?
-      let args = Js.Array.concat(Config.Connection.getCommandLineOptions(), ["--interaction"])
-
+      let args = Array.concat(["--interaction"], Config.Connection.getCommandLineOptions())
       switch await ProcInfo.make(path, args) {
       | Error(e) => Error(e)
       | Ok(procInfo) =>
diff --git a/src/Parser/Parser.res b/src/Parser/Parser.res
index 6b882cce..65b2d6a0 100644
--- a/src/Parser/Parser.res
+++ b/src/Parser/Parser.res
@@ -119,7 +119,10 @@ module SExpression = {
     | L(xs) => xs->Array.map(flatten)->Array.concatMany
     }
 
-  let parseWithContinuation = (string: string): Incr.continuation<t, (SExprParseError.t, string)> => {
+  let parseWithContinuation = (string: string): Incr.continuation<
+    t,
+    (SExprParseError.t, string),
+  > => {
     let rec parseSExpression = (state: state, string: string): Incr.continuation<
       t,
       (SExprParseError.t, string),
@@ -256,19 +259,6 @@ module Error = {
     }
 }
 
-let userInputToSExpr = (s: string): string =>
-  Js.String.trim(
-    Js.String.replaceByRe(
-      %re("/\n/g"),
-      "\\n",
-      Js.String.replaceByRe(
-        %re("/\r\n/g"),
-        "\\r\\n",
-        Js.String.replaceByRe(%re("/\"/g"), "\\\"", Js.String.replaceByRe(%re("/\\/g"), "\\\\", s)),
-      ),
-    ),
-  )
-
 let filepath = s => {
   // remove the Windows Bidi control character
   let removedBidi = if Js.String.charCodeAt(0, s) === 8234.0 {
@@ -285,3 +275,33 @@ let filepath = s => {
 
   replaced
 }
+
+// Escapes human-readable strings to Agda-readable strings,
+// by inserting backslashes before the following characters:
+//
+//      LF      => \n
+//      CR LF   => \r\n
+//      "       -> \"
+//      \       -> \\
+
+let escape = (s: string): string =>
+  Js.String.trim(
+    Js.String.replaceByRe(
+      %re("/\n/g"),
+      "\\n",
+      Js.String.replaceByRe(
+        %re("/\r\n/g"),
+        "\\r\\n",
+        Js.String.replaceByRe(%re("/\"/g"), "\\\"", Js.String.replaceByRe(%re("/\\/g"), "\\\\", s)),
+      ),
+    ),
+  )
+
+// Almost the inverse of escape, but only for EOL characters.
+//
+//      \n    => LF
+//      \r\n  => CR LF
+let unescapeEOL = (s: string): string =>
+  s
+  ->String.replaceRegExp(%re("/\\r\\n/g"), "\r\n")
+  ->String.replaceRegExp(%re("/\\n/g"), "\n")
diff --git a/src/Request.res b/src/Request.res
index b5ca76c5..a205caa2 100644
--- a/src/Request.res
+++ b/src/Request.res
@@ -141,7 +141,7 @@ let encode = (
     }
   | SearchAbout(normalization, expr) =>
     let normalization = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
     `${commonPart(NonInteractive)}( Cmd_search_about_toplevel ${normalization} "${content}" )`
 
   // Related issue and commit of agda/agda
@@ -149,7 +149,7 @@ let encode = (
   // https://github.com/agda/agda/commit/021e6d24f47bac462d8bc88e2ea685d6156197c4
   | Give(goal) =>
     let index: string = string_of_int(goal.index)
-    let content: string = Goal.getContent(goal, document)->Parser.userInputToSExpr
+    let content: string = Goal.getContent(goal, document)->Parser.escape
     let range: string = buildRange(goal)
     if Util.Version.gte(version, "2.5.3") {
       `${commonPart(NonInteractive)}( Cmd_give WithoutForce ${index} ${range} "${content}" )`
@@ -159,14 +159,14 @@ let encode = (
 
   | Refine(goal) =>
     let index: string = string_of_int(goal.index)
-    let content: string = Goal.getContent(goal, document)->Parser.userInputToSExpr
+    let content: string = Goal.getContent(goal, document)->Parser.escape
     let range: string = buildRange(goal)
     `${commonPart(NonInteractive)}( Cmd_refine_or_intro False ${index} ${range} "${content}" )`
 
   | ElaborateAndGive(normalization, expr, goal) =>
     let index = string_of_int(goal.index)
     let normalization = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(
         NonInteractive,
@@ -175,7 +175,7 @@ let encode = (
   | Auto(normalization, goal) =>
     let normalization = Command.Normalization.encode(normalization)
     let index: string = string_of_int(goal.index)
-    let content: string = Goal.getContent(goal, document)->Parser.userInputToSExpr
+    let content: string = Goal.getContent(goal, document)->Parser.escape
     let range: string = buildRange(goal)
 
     if Util.Version.gte(version, "2.7.0") {
@@ -194,14 +194,14 @@ let encode = (
 
   | Case(goal) =>
     let index: string = string_of_int(goal.index)
-    let content: string = Goal.getContent(goal, document)->Parser.userInputToSExpr
+    let content: string = Goal.getContent(goal, document)->Parser.escape
     let range: string = buildRange(goal)
     `${commonPart(NonInteractive)}( Cmd_make_case ${index} ${range} "${content}" )`
 
   | HelperFunctionType(normalization, expr, goal) =>
     let index = string_of_int(goal.index)
     let normalization = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(
         NonInteractive,
@@ -210,12 +210,12 @@ let encode = (
   | InferType(normalization, expr, goal) =>
     let index = string_of_int(goal.index)
     let normalization = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
     `${commonPart(NonInteractive)}( Cmd_infer ${normalization} ${index} noRange "${content}" )`
 
   | InferTypeGlobal(normalization, expr) =>
     let normalization = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(None)}( Cmd_infer_toplevel ${normalization} "${content}" )`
 
@@ -237,7 +237,7 @@ let encode = (
   | GoalTypeContextAndInferredType(normalization, expr, goal) =>
     let index: string = string_of_int(goal.index)
     let normalization: string = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(
         NonInteractive,
@@ -246,7 +246,7 @@ let encode = (
   | GoalTypeContextAndCheckedType(normalization, expr, goal) =>
     let index: string = string_of_int(goal.index)
     let normalization: string = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(
         NonInteractive,
@@ -255,7 +255,7 @@ let encode = (
   | ModuleContents(normalization, expr, goal) =>
     let index: string = string_of_int(goal.index)
     let normalization: string = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(
         NonInteractive,
@@ -263,7 +263,7 @@ let encode = (
 
   | ModuleContentsGlobal(normalization, expr) =>
     let normalization: string = Command.Normalization.encode(normalization)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     `${commonPart(None)}( Cmd_show_module_contents_toplevel ${normalization} "${content}" )`
 
@@ -271,7 +271,7 @@ let encode = (
     let index: string = string_of_int(goal.index)
     let ignoreAbstract: string = string_of_bool(Command.ComputeMode.ignoreAbstract(computeMode))
     let computeMode: string = Command.ComputeMode.encode(computeMode)
-    let content: string = Parser.userInputToSExpr(expr)
+    let content: string = Parser.escape(expr)
 
     if Util.Version.gte(version, "2.5.2") {
       `${commonPart(NonInteractive)}( Cmd_compute ${computeMode} ${index} noRange "${content}" )`
@@ -282,7 +282,7 @@ let encode = (
   | ComputeNormalFormGlobal(computeMode, expr) =>
     let ignoreAbstract: string = string_of_bool(Command.ComputeMode.ignoreAbstract(computeMode))
     let computeMode: string = Command.ComputeMode.encode(computeMode)
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
 
     if Util.Version.gte(version, "2.5.2") {
       `${commonPart(NonInteractive)}( Cmd_compute_toplevel ${computeMode} "${content}" )`
@@ -292,12 +292,12 @@ let encode = (
 
   | WhyInScope(expr, goal) =>
     let index: string = string_of_int(goal.index)
-    let content: string = Parser.userInputToSExpr(expr)
+    let content: string = Parser.escape(expr)
 
     `${commonPart(NonInteractive)}( Cmd_why_in_scope ${index} noRange "${content}" )`
 
   | WhyInScopeGlobal(expr) =>
-    let content = Parser.userInputToSExpr(expr)
+    let content = Parser.escape(expr)
     `${commonPart(None)}( Cmd_why_in_scope_toplevel "${content}" )`
   }
 }
diff --git a/src/Response.res b/src/Response.res
index ccb30ea1..6a2987b1 100644
--- a/src/Response.res
+++ b/src/Response.res
@@ -83,7 +83,7 @@ module DisplayInfo = {
     | Some(A(rawPayload)) =>
       // there are some explicitly escaped EOLs like "\n" or "\r\n" in the s-expressions
       // we need to replace them with actual EOLs
-      let payload = rawPayload->String.replaceRegExp(%re("/\\n|\\r\\n/g"), "\n")
+      let payload = Parser.unescapeEOL(rawPayload)
       switch xs[0] {
       | Some(A("*Compilation result*")) => Some(CompilationOk(payload))
       | Some(A("*Constraints*")) =>
@@ -285,7 +285,7 @@ let parse = (tokens: Token.t): result<t, Parser.Error.t> => {
         switch xs[3] {
         | Some(A("t")) =>
           switch xs[2] {
-          | Some(A(message)) => Ok(RunningInfo(1, message))
+          | Some(A(message)) => Ok(RunningInfo(1, Parser.unescapeEOL(message)))
           | _ => err(11)
           }
         | _ => Ok(ClearRunningInfo)
@@ -298,7 +298,7 @@ let parse = (tokens: Token.t): result<t, Parser.Error.t> => {
       }
     | Some(A("agda2-verbose")) =>
       switch xs[1] {
-      | Some(A(message)) => Ok(RunningInfo(2, message))
+      | Some(A(message)) => Ok(RunningInfo(2, Parser.unescapeEOL(message)))
       | _ => err(13)
       }
     // NOTE: now there are 2 kinds of "agda2-highlight-clear", "TokenBased" and "NotOnlyTokenBased"
diff --git a/src/State/State__Goal.res b/src/State/State__Goal.res
index ac172e00..302a065a 100644
--- a/src/State/State__Goal.res
+++ b/src/State/State__Goal.res
@@ -7,6 +7,7 @@ module type Module = {
   let pointed: State.t => option<(Goal.t, string)>
   let replaceWithLines: (State.t, Goal.t, array<string>) => promise<unit>
   let replaceWithLambda: (State.t, Goal.t, array<string>) => promise<unit>
+  let indentationWidth: (VSCode.TextDocument.t, Goal.t) => (int, string, VSCode.Range.t)
   let caseSplitAux: (VSCode.TextDocument.t, AgdaModeVscode.Goal.t) => (bool, int, Interval.t)
 
   let redecorate: State.t => unit
@@ -288,11 +289,6 @@ module Module: Module = {
 
   let pointed = (state: State.t): option<(Goal.t, string)> => {
     updateIntervals(state)
-
-    // let cursor = switch cursor {
-    // | None => Editor.Cursor.get(state.editor)
-    // | Some(x) => x
-    // }
     let cursor = Editor.Cursor.get(state.editor)
     let cursorOffset = state.document->VSCode.TextDocument.offsetAt(cursor)
     let pointedGoals =
diff --git a/src/State/State__Response.res b/src/State/State__Response.res
index 35ba695b..bd099490 100644
--- a/src/State/State__Response.res
+++ b/src/State/State__Response.res
@@ -1,5 +1,10 @@
 // from Agda Response to Tasks
-let removeNewlines = string => string->String.split("\n")->Array.join("\n")
+
+// adds indentation to a multiline string
+let indent = (content, indent) => {
+  let indentation = String.repeat(" ", indent)
+  content->String.replaceRegExp(%re("/\n/g"), "\n" ++ indentation) // should also handles CR LF on Windows
+}
 
 open Response
 module DisplayInfo = {
@@ -131,8 +136,7 @@ let rec handle = async (
         let point = state.document->VSCode.TextDocument.positionAt(offset - 1)
         Editor.Cursor.set(state.editor, point)
       }
-    | InteractionPoints(indices) => 
-      await State__Goal.instantiate(state, indices)
+    | InteractionPoints(indices) => await State__Goal.instantiate(state, indices)
     | GiveAction(index, give) =>
       let found = state.goals->Array.filter(goal => goal.index == index)
       switch found[0] {
@@ -151,8 +155,17 @@ let rec handle = async (
           // do nothing
           await State__Goal.removeBoundaryAndDestroy(state, goal)
         | GiveString(content) =>
+          let (indentationWidth, _text, _) = State__Goal.indentationWidth(state.document, goal)
+          // 1. ideally, we want to add "\t" or equivalent spaces based on
+          //    "editor.tabSize" and "editor.insertSpaces"
+          //    but we cannot load the "editor.tabSize" here
+          //    so as a workaround, we use a default value of 2
+          //    maybe consider storing these attributes in the state in the future
+          // 2. the Emacs plugin seems to use len(text) as the indent, which could be a
+          //    safer choice
+          let defaultIndentation = 2
           await State__Goal.modify(state, goal, _ =>
-            Js.String.replaceByRe(%re("/\\\\n/g"), "\n", content)
+            Parser.unescapeEOL(content)->indent(defaultIndentation + indentationWidth)
           )
           await State__Goal.removeBoundaryAndDestroy(state, goal)
         }
@@ -167,7 +180,7 @@ let rec handle = async (
         }
         // dispatch `agda-mode:load` but do it asynchronously
         // so that we can finish let `agda-mode:case` finish first
-        dispatchCommand(Load)->ignore 
+        dispatchCommand(Load)->ignore
       }
     | SolveAll(solutions) =>
       let solveOne = async ((index, solution)) => {
@@ -192,15 +205,13 @@ let rec handle = async (
       }
     | DisplayInfo(info) => await DisplayInfo.handle(state, info)
     | RunningInfo(1, message) =>
-      let message = removeNewlines(message)
       await State.View.Panel.displayInAppendMode(
         state,
         Plain("Type-checking"),
         [Item.plainText(message)],
       )
     | RunningInfo(verbosity, message) =>
-      let message = removeNewlines(message)
-      state.runningInfoLog->Js.Array2.push((verbosity, message))->ignore
+      state.runningInfoLog->Array.push((verbosity, message))->ignore
       await State.View.DebugBuffer.displayInAppendMode([(verbosity, message)])
     | CompleteHighlightingAndMakePromptReappear =>
       // apply decoration before handling Last Responses
diff --git a/test/tests/Parser/Response/Issue95-2.6.1-Unix.out b/test/tests/Parser/Response/Issue95-2.6.1-Unix.out
index 90bf728a..164530ed 100644
--- a/test/tests/Parser/Response/Issue95-2.6.1-Unix.out
+++ b/test/tests/Parser/Response/Issue95-2.6.1-Unix.out
@@ -1,7 +1,8 @@
 NonLast Status: implicit arguments not displayed, module not type checked
 NonLast ClearRunningInfo
 NonLast ClearHighlighting
-NonLast RunningInfo 1 Checking Issue95 (/Users/omega/github/agda-mode/test/ManualTests/Issue95.agda).\n
+NonLast RunningInfo 1 Checking Issue95 (/Users/omega/github/agda-mode/test/ManualTests/Issue95.agda).
+
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-0
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-1
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-2
diff --git a/test/tests/Parser/Response/QuotationMark-2.6.0-Unix.out b/test/tests/Parser/Response/QuotationMark-2.6.0-Unix.out
index a8b2739d..80dc5b60 100644
--- a/test/tests/Parser/Response/QuotationMark-2.6.0-Unix.out
+++ b/test/tests/Parser/Response/QuotationMark-2.6.0-Unix.out
@@ -1,7 +1,8 @@
 NonLast Status: implicit arguments not displayed, module not type checked
 NonLast ClearRunningInfo
 NonLast ClearHighlighting
-NonLast RunningInfo 1 Checking QuotationMark (/Users/omega/github/agda-mode/test/ManualTests/QuotationMark.agda).\n
+NonLast RunningInfo 1 Checking QuotationMark (/Users/omega/github/agda-mode/test/ManualTests/QuotationMark.agda).
+
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-0
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-1
 NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-2
diff --git a/test/tests/Parser/Test__Parser.res b/test/tests/Parser/Test__Parser.res
index f2e37b37..8f9bb828 100644
--- a/test/tests/Parser/Test__Parser.res
+++ b/test/tests/Parser/Test__Parser.res
@@ -1,32 +1,47 @@
 open Mocha
 
-describe("when running Parser.userInputToSExpr", () => {
+describe("when running Parser.escape", () => {
   it("should make escaped backslash explicit", () => {
     let raw = "\\ x -> x"
     let expected = "\\\\ x -> x"
-    let actual = Parser.userInputToSExpr(raw)
+    let actual = Parser.escape(raw)
     Assert.deepEqual(actual, expected)
   })
 
   it("should make escaped newline on Unix explicit", () => {
     let raw = "x\ny"
     let expected = "x\\ny"
-    let actual = Parser.userInputToSExpr(raw)
+    let actual = Parser.escape(raw)
     Assert.deepEqual(actual, expected)
   })
 
   it("should make escaped newline on Windows explicit", () => {
     let raw = "x\r\ny"
     let expected = "x\\r\\ny"
-    let actual = Parser.userInputToSExpr(raw)
+    let actual = Parser.escape(raw)
     Assert.deepEqual(actual, expected)
   })
 
   it("should make escaped double quote explicit", () => {
     let raw = "\"x\""
     let expected = "\\\"x\\\""
-    let actual = Parser.userInputToSExpr(raw)
+    let actual = Parser.escape(raw)
     Assert.deepEqual(actual, expected)
   })
+})
 
-})
\ No newline at end of file
+describe("when running Parser.unescapeEOL", () => {
+  it("should make explicit newline on Unix implicit", () => {
+    let raw = "x\\ny"
+    let expected = "x\ny"
+    let actual = Parser.unescapeEOL(raw)
+    Assert.deepEqual(actual, expected)
+  })
+
+  it("should make explicit newline on Windows implicit", () => {
+    let raw = "x\\r\\ny"
+    let expected = "x\r\ny"
+    let actual = Parser.unescapeEOL(raw)
+    Assert.deepEqual(actual, expected)
+  })
+})
diff --git a/test/tests/Test__Auto.res b/test/tests/Test__Auto.res
index 25028092..38dcbb11 100644
--- a/test/tests/Test__Auto.res
+++ b/test/tests/Test__Auto.res
@@ -7,19 +7,17 @@ let run = normalization => {
       Async.it(
         "should be responded with the correct answer 1",
         async () => {
-          let ctx = await AgdaMode.make("Auto.agda")
-          let state = await ctx->AgdaMode.load
-
+          let ctx = await AgdaMode.makeAndLoad("Auto.agda")
           let responses = ref([])
           let responseHandler = async response => responses.contents->Array.push(response)
 
-          switch state.goals[0] {
+          switch ctx.state.goals[0] {
           | Some(goal) =>
-            await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal))
+            await ctx.state->State.sendRequest(responseHandler, Request.Auto(normalization, goal))
           | None => Assert.fail("No goals found")
           }
 
-          switch state.agdaVersion {
+          switch ctx.state.agdaVersion {
           | Some(version) =>
             if Util.Version.gte(version, "2.7.0") {
               Assert.deepEqual(
@@ -50,19 +48,18 @@ let run = normalization => {
       Async.it(
         "should be responded with the correct answer 2",
         async () => {
-          let ctx = await AgdaMode.make("Auto.agda")
-          let state = await ctx->AgdaMode.load
+          let ctx = await AgdaMode.makeAndLoad("Auto.agda")
 
           let responses = ref([])
           let responseHandler = async response => responses.contents->Array.push(response)
 
-          switch state.goals[1] {
+          switch ctx.state.goals[1] {
           | Some(goal) =>
-            await state->State.sendRequest(responseHandler, Request.Auto(normalization, goal))
+            await ctx.state->State.sendRequest(responseHandler, Request.Auto(normalization, goal))
           | None => Assert.fail("No goals found")
           }
 
-          switch state.agdaVersion {
+          switch ctx.state.agdaVersion {
           | Some(version) =>
             if Util.Version.gte(version, "2.7.0") {
               Assert.deepEqual(
diff --git a/test/tests/Test__CaseSplit.res b/test/tests/Test__CaseSplit.res
index 07834c30..d1594a8a 100644
--- a/test/tests/Test__CaseSplit.res
+++ b/test/tests/Test__CaseSplit.res
@@ -42,14 +42,12 @@ describe("agda-mode:case", () => {
   This.timeout(10000)
   let fileContent = ref("")
 
-  Async.before(() => readFile(Path.asset("CaseSplit.agda"), fileContent))
-  Async.after(() => restoreFile(Path.asset("CaseSplit.agda"), fileContent))
+  Async.before(async () => fileContent := (await File.read(Path.asset("CaseSplit.agda"))))
+  Async.after(async () => await File.write(Path.asset("CaseSplit.agda"), fileContent.contents))
 
   Async.it("should have more goals after splitting", async () => {
-    let ctx = await AgdaMode.make("CaseSplit.agda")
-    let state = await ctx->AgdaMode.load
-    let state = await ctx->AgdaMode.case(Some(VSCode.Position.make(7, 16), "x"), state)
-    Assert.deepEqual(Array.length(state.goals), 10)
-
+    let ctx = await AgdaMode.makeAndLoad("CaseSplit.agda")
+    await ctx->AgdaMode.case(Some(VSCode.Position.make(7, 16), "x"))
+    Assert.deepEqual(Array.length(ctx.state.goals), 10)
   })
 })
diff --git a/test/tests/Test__ComputeNormalForm.res b/test/tests/Test__ComputeNormalForm.res
index 1b5d665c..17c0a80d 100644
--- a/test/tests/Test__ComputeNormalForm.res
+++ b/test/tests/Test__ComputeNormalForm.res
@@ -2,61 +2,54 @@ open Mocha
 open Test__Util
 
 let run = normalization =>
-    describe("request to Agda", () => {
-      describe(
-        "global",
-        () => {
-          Async.it(
-            "should be responded with the correct answer",
-            async () => {
-              let ctx = await AgdaMode.make("ComputeNormalForm.agda")
-              let state = await ctx->AgdaMode.load
-
-              let responses = ref([])
-              let responseHandler = async response => responses.contents->Array.push(response)
-              await state->State.sendRequest(
-                responseHandler,
-                Request.ComputeNormalFormGlobal(normalization, "Z + S Z"),
-              )
-
-              Assert.deepEqual(
-                responses.contents,
-                [
-                  Status(false, false),
-                  DisplayInfo(NormalForm("S Z")),
-                  CompleteHighlightingAndMakePromptReappear,
-                ],
-              )
-            },
+  describe("request to Agda", () => {
+    describe("global", () => {
+      Async.it(
+        "should be responded with the correct answer",
+        async () => {
+          let ctx = await AgdaMode.makeAndLoad("ComputeNormalForm.agda")
+
+          let responses = ref([])
+          let responseHandler = async response => responses.contents->Array.push(response)
+          await ctx.state->State.sendRequest(
+            responseHandler,
+            Request.ComputeNormalFormGlobal(normalization, "Z + S Z"),
           )
 
-          Async.it(
-            "should be responded with the correct answer",
-            async () => {
-              let ctx = await AgdaMode.make("ComputeNormalForm.agda")
-              let state = await ctx->AgdaMode.load
+          Assert.deepEqual(
+            responses.contents,
+            [
+              Status(false, false),
+              DisplayInfo(NormalForm("S Z")),
+              CompleteHighlightingAndMakePromptReappear,
+            ],
+          )
+        },
+      )
 
-              let responses = ref([])
-              let responseHandler = async response => responses.contents->Array.push(response)
-              await state->State.sendRequest(
-                responseHandler,
-                Request.ComputeNormalFormGlobal(normalization, "S Z + S Z"),
-              )
+      Async.it(
+        "should be responded with the correct answer",
+        async () => {
+          let ctx = await AgdaMode.makeAndLoad("ComputeNormalForm.agda")
+          let responses = ref([])
+          let responseHandler = async response => responses.contents->Array.push(response)
+          await ctx.state->State.sendRequest(
+            responseHandler,
+            Request.ComputeNormalFormGlobal(normalization, "S Z + S Z"),
+          )
 
-              Assert.deepEqual(
-                responses.contents,
-                [
-                  Status(false, false),
-                  DisplayInfo(NormalForm("S (S Z)")),
-                  CompleteHighlightingAndMakePromptReappear,
-                ],
-              )
-            },
+          Assert.deepEqual(
+            responses.contents,
+            [
+              Status(false, false),
+              DisplayInfo(NormalForm("S (S Z)")),
+              CompleteHighlightingAndMakePromptReappear,
+            ],
           )
         },
       )
     })
-
+  })
 
 describe("agda-mode.compute-normal-form[DefaultCompute]", () => {
   run(DefaultCompute)
@@ -64,4 +57,4 @@ describe("agda-mode.compute-normal-form[DefaultCompute]", () => {
 
 describe("agda-mode.compute-normal-form[IgnoreAbstract]", () => {
   run(IgnoreAbstract)
-})
\ No newline at end of file
+})
diff --git a/test/tests/Test__Refine.res b/test/tests/Test__Refine.res
new file mode 100644
index 00000000..8ff0fa02
--- /dev/null
+++ b/test/tests/Test__Refine.res
@@ -0,0 +1,23 @@
+open Mocha
+open Test__Util
+
+describe("agda-mode.refine", () => {
+  describe("Issue #158", () => {
+
+    let fileContent = ref("")
+
+    Async.before(async () => fileContent := (await File.read(Path.asset("Issue158.agda"))))
+    Async.after(async () => await File.write(Path.asset("Issue158.agda"), fileContent.contents))
+
+    Async.it(
+      "should be result in the correct refinement",
+      async () => {
+        let ctx = await AgdaMode.makeAndLoad("Issue158.agda")
+        await ctx->AgdaMode.refine(~cursor=VSCode.Position.make(12, 9))
+        let actual = await File.read(Path.asset("Issue158.agda"))
+        let expected = await File.read(Path.asset("Issue158.agda.out"))
+        Assert.equal(actual, expected)
+      },
+    )
+  })
+})
diff --git a/test/tests/Test__Tokens.res b/test/tests/Test__Tokens.res
index fca5b7b3..98c06818 100644
--- a/test/tests/Test__Tokens.res
+++ b/test/tests/Test__Tokens.res
@@ -7,10 +7,9 @@ describe("Tokens", () => {
     Async.it(
       "should produce 28 tokens",
       async () => {
-        let ctx = await AgdaMode.make("GotoDefinition.agda")
-        let state = await ctx->AgdaMode.load
+        let ctx = await AgdaMode.makeAndLoad("GotoDefinition.agda")
         let tokens =
-          state.tokens
+          ctx.state.tokens
           ->Tokens.toArray
           ->Array.map(
             ((token, range)) => Editor.Range.toString(range) ++ " " ++ Tokens.Token.toString(token),
@@ -22,10 +21,9 @@ describe("Tokens", () => {
     Async.it(
       "should produce correct tokens",
       async () => {
-        let ctx = await AgdaMode.make("GotoDefinition.agda")
-        let state = await ctx->AgdaMode.load
+        let ctx = await AgdaMode.makeAndLoad("GotoDefinition.agda")
         let tokens =
-          state.tokens
+          ctx.state.tokens
           ->Tokens.toArray
           ->Array.map(
             ((token, range)) => Editor.Range.toString(range) ++ " " ++ Tokens.Token.toString(token),
diff --git a/test/tests/Test__Util.res b/test/tests/Test__Util.res
index 1b032703..ccbd2eae 100644
--- a/test/tests/Test__Util.res
+++ b/test/tests/Test__Util.res
@@ -4,6 +4,34 @@ open Js.Promise
 
 exception Exn(string)
 
+module File = {
+  let open_ = (fileName): promise<VSCode.TextEditor.t> =>
+    VSCode.Window.showTextDocumentWithUri(VSCode.Uri.file(fileName), None)
+
+  let read = async (fileName): string => {
+    let editor = await open_(fileName)
+    let document = VSCode.TextEditor.document(editor)
+    VSCode.TextDocument.getText(document, None)
+  }
+
+  let write = async (fileName, content) => {
+    let editor = await open_(fileName)
+    let document = VSCode.TextEditor.document(editor)
+
+    let lineCount = document->VSCode.TextDocument.lineCount
+    let replaceRange = VSCode.Range.make(
+      VSCode.Position.make(0, 0),
+      VSCode.Position.make(lineCount, 0),
+    )
+    let succeed = await Editor.Text.replace(document, replaceRange, content)
+    if succeed {
+      let _ = await VSCode.TextDocument.save(document)
+    } else {
+      raise(Failure("Failed to write to " ++ fileName))
+    }
+  }
+}
+
 // wrapper around BsMocha's Assertions
 let runner: (unit => unit) => promise<result<'a, exn>> = %raw(` function(f) {
     var tmp
@@ -57,17 +85,14 @@ let activateExtension = (): State__Type.channels => {
   }
 }
 
-let openFile = (fileName): Promise.t<VSCode.TextEditor.t> =>
-  VSCode.Window.showTextDocumentWithUri(VSCode.Uri.file(fileName), None)
-
 let activateExtensionAndOpenFile = async fileName => {
   let channels = activateExtension()
-  let editor = await openFile(fileName)
+  let editor = await File.open_(fileName)
   (editor, channels)
 }
 
 @module("vscode") @scope("commands")
-external executeCommand: string => Promise.t<option<result<State.t, Connection.Error.t>>> =
+external executeCommand: string => promise<option<result<State.t, Connection.Error.t>>> =
   "executeCommand"
 
 let wait = ms => Promise.make((resolve, _) => Js.Global.setTimeout(resolve, ms)->ignore)
@@ -272,55 +297,62 @@ module AgdaMode = {
   type t = {
     filepath: string,
     channels: State__Type.channels,
+    mutable state: State__Type.t,
   }
 
-  let make = async (~als=false, filepath) => {
+  let makeAndLoad = async (~als=false, filepath) => {
     let filepath = Path.asset(filepath)
     // for mocking Configs
     Config.inTestingMode := true
     // set name for searching Agda
     await Config.Connection.setAgdaVersion("agda")
     await Config.Connection.setUseAgdaLanguageServer(als)
-    let _ = await exists("agda")
-    {
-      filepath,
-      channels: activateExtension(),
+    // make sure that "agda" exists in PATH
+    await exists("agda")
+    //
+    let load = async (channels: State__Type.channels, filepath) => {
+      let (promise, resolve, _) = Util.Promise_.pending()
+
+      // agda-mode:load is consider finished
+      // when `CompleteHighlightingAndMakePromptReappear` has been handled
+      let disposable = channels.responseHandled->Chan.on(response => {
+        switch response {
+        | CompleteHighlightingAndMakePromptReappear => resolve()
+        | _ => ()
+        }
+      })
+
+      let _ = await File.open_(filepath) // need to open the file first somehow
+      switch await executeCommand("agda-mode.load") {
+      | None => raise(Failure("Cannot load " ++ filepath))
+      | Some(Ok(state)) =>
+        await promise
+        disposable() // stop listening to responses
+        state
+      | Some(Error(error)) =>
+        let (header, body) = Connection.Error.toString(error)
+        raise(Failure(header ++ "\n" ++ body))
+      }
     }
-  }
-
-  let load = async self => {
-    let (promise, resolve, _) = Util.Promise_.pending()
 
-    // agda-mode:load is consider finished
-    // when `CompleteHighlightingAndMakePromptReappear` has been handled
-    let disposable = self.channels.responseHandled->Chan.on(response => {
-      switch response {
-      | CompleteHighlightingAndMakePromptReappear => resolve()
-      | _ => ()
-      }
-    })
+    let channels = activateExtension()
+    let state = await load(channels, filepath)
 
-    let _ = await openFile(self.filepath)
-    switch await executeCommand("agda-mode.load") {
-    | None => raise(Failure("Cannot load " ++ self.filepath))
-    | Some(Ok(state)) =>
-      await promise
-      disposable() // stop listening to responses
-      state
-    | Some(Error(error)) =>
-      let (header, body) = Connection.Error.toString(error)
-      raise(Failure(header ++ "\n" ++ body))
+    {
+      filepath,
+      channels,
+      state,
     }
   }
 
-  let case = async (self, cursorAndPayload, state: State__Type.t) => {
-    let editor = await openFile(self.filepath)
+  let case = async (self, cursorAndPayload) => {
+    let editor = await File.open_(self.filepath)
 
     // set cursor and insert the target for case splitting
     switch cursorAndPayload {
     | None => ()
     | Some(cursor, payload) =>
-      let succeed = await Editor.Text.insert(state.document, cursor, payload)
+      let succeed = await Editor.Text.insert(self.state.document, cursor, payload)
       if !succeed {
         raise(Failure("Failed to insert text"))
       }
@@ -330,7 +362,7 @@ module AgdaMode = {
     // The `agda-mode.load` command will be issued after `agda-mode.case` is executed
     // listen to the `agda-mode.load` command to know when the whole case split process is done
     let (promise, resolve, _) = Util.Promise_.pending()
-    let destructor = state.channels.commandHandled->Chan.on(command => {
+    let destructor = self.state.channels.commandHandled->Chan.on(command => {
       switch command {
       | Command.Load => resolve()
       | _ => ()
@@ -345,67 +377,34 @@ module AgdaMode = {
       // stop listening to commands
       destructor()
 
-      // resolve the promise
-      state
+      // update the context with the new state
+      self.state = state
     | Some(Error(error)) =>
       let (header, body) = Connection.Error.toString(error)
       raise(Failure(header ++ "\n" ++ body))
     }
   }
 
-  let refine = async (self, cursorAndPayload, state: State__Type.t): AgdaModeVscode.State.t => {
-    let editor = await openFile(self.filepath)
-    switch cursorAndPayload {
+  let refine = async (self, ~cursor=?, ~payload=?) => {
+    let editor = await File.open_(self.filepath)
+    // edit the file
+    switch cursor {
     | None => ()
-    | Some(cursor, None) => Editor.Cursor.set(editor, cursor)
-    | Some(cursor, Some(payload)) =>
-      let _ = await Editor.Text.insert(state.document, cursor, payload)
+    | Some(cursor) =>
+      switch payload {
+      | None => ()
+      | Some(payload) =>
+        let _ = await Editor.Text.insert(self.state.document, cursor, payload)
+      }
       Editor.Cursor.set(editor, cursor)
     }
+
     switch await executeCommand("agda-mode.refine") {
     | None => raise(Failure("Cannot case refine " ++ self.filepath))
-    | Some(Ok(state)) => state
+    | Some(Ok(state)) => self.state = state
     | Some(Error(error)) =>
       let (header, body) = Connection.Error.toString(error)
       raise(Failure(header ++ "\n" ++ body))
     }
   }
 }
-
-// store file content before testing so that we can restore it later
-let readFile = async (filepath, var) => {
-  let editor = await openFile(filepath)
-  var := Editor.Text.getAll(VSCode.TextEditor.document(editor))
-}
-
-let restoreFile = async (filepath, var) => {
-  let editor = await openFile(filepath)
-  let document = VSCode.TextEditor.document(editor)
-  let lineCount = document->VSCode.TextDocument.lineCount
-  let replaceRange = VSCode.Range.make(
-    VSCode.Position.make(0, 0),
-    VSCode.Position.make(lineCount, 0),
-  )
-  let succeed = await Editor.Text.replace(document, replaceRange, var.contents)
-  if succeed {
-    let _ = await VSCode.TextDocument.save(document)
-  } else {
-    raise(Failure("Failed to restore the file"))
-  }
-}
-
-module R = {
-  let unwrap = (x: result<'a, 'e>): 'a =>
-    switch x {
-    | Ok(x) => x
-    | Error(error) => raise(error)
-    }
-}
-
-// for handling promise<result<'a, 'error>> in tests
-module P = {
-  let unwrap = async (promise: promise<result<'a, 'e>>): 'a => {
-    let result = await promise
-    R.unwrap(result)
-  }
-}
diff --git a/test/tests/assets/Issue158.agda b/test/tests/assets/Issue158.agda
new file mode 100644
index 00000000..d44ee7d8
--- /dev/null
+++ b/test/tests/assets/Issue158.agda
@@ -0,0 +1,13 @@
+module Issue158 where
+
+postulate
+  A : Set
+
+record Foo : Set where
+  field
+    very-long-field-name-1 : A
+    very-long-field-name-2 : A
+    very-long-field-name-3 : A
+
+foo : Foo
+foo = {!   !}
\ No newline at end of file
diff --git a/test/tests/assets/Issue158.agda.out b/test/tests/assets/Issue158.agda.out
new file mode 100644
index 00000000..0006b16d
--- /dev/null
+++ b/test/tests/assets/Issue158.agda.out
@@ -0,0 +1,17 @@
+module Issue158 where
+
+postulate
+  A : Set
+
+record Foo : Set where
+  field
+    very-long-field-name-1 : A
+    very-long-field-name-2 : A
+    very-long-field-name-3 : A
+
+foo : Foo
+foo = record
+  { very-long-field-name-1 = {!   !}
+  ; very-long-field-name-2 = {!   !}
+  ; very-long-field-name-3 = {!   !}
+  }
\ No newline at end of file