diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean
index 0b25b34232..e3d84fe494 100644
--- a/tests/lean/server/edits.lean
+++ b/tests/lean/server/edits.lean
@@ -2,8 +2,6 @@ import Lean.Data.Lsp
 open IO Lean Lsp
 
 def main : IO Unit := do
-  pure ()
-#exit
   Ipc.runWith (←IO.appPath) #["--server"] do
     let hIn ← Ipc.stdin
     hIn.write (←FS.readBinFile "init_vscode_1_47_2.log")
@@ -26,7 +24,7 @@ def main : IO Unit := do
       FS.writeFile "edits_diag.json.produced" (toString <| toJson (diag : JsonRpc.Message))
 
       if let some (refDiag : JsonRpc.Notification PublishDiagnosticsParams) :=
-        (Json.parse $ ←FS.readFile "edits_diag.json").toOption >>= fromJson?
+        (Json.parse $ ←FS.readFile "edits_diag.json") >>= fromJson?
       then
         assert! (diag == refDiag)
       else
diff --git a/tests/lean/server/edits_diag.json b/tests/lean/server/edits_diag.json
index 1d4260cc3d..64d58db7d7 100644
--- a/tests/lean/server/edits_diag.json
+++ b/tests/lean/server/edits_diag.json
@@ -2,39 +2,37 @@
  {"version": 7,
   "uri": "file:///test.lean",
   "diagnostics":
-  [{"tags": null,
-    "source": "Lean 4 server",
+  [{"source": "Lean 4",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 6}},
     "message": "n : Nat",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "fullRange":
+    {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 6}}},
+   {"source": "Lean 4",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 6}},
     "message": "s : String",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "fullRange":
+    {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 6}}},
+   {"source": "Lean 4",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 12, "character": 0},
      "end": {"line": 12, "character": 5}},
     "message": "Hello world!\n",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "fullRange":
+    {"start": {"line": 12, "character": 0},
+     "end": {"line": 12, "character": 5}}},
+   {"source": "Lean 4",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 16, "character": 0},
      "end": {"line": 16, "character": 6}},
     "message": "def α : Unit :=\n()",
-    "code": null}]},
+    "fullRange":
+    {"start": {"line": 16, "character": 0},
+     "end": {"line": 16, "character": 6}}}]},
  "method": "textDocument/publishDiagnostics",
- "jsonrpc": "2.0"}
+ "jsonrpc": "2.0"}
\ No newline at end of file