From 2de5b141ebf44c1cccbea4393409a67b7ee450f5 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 7 Apr 2021 16:49:08 +0200
Subject: [PATCH] test: interactive: support inserting text

---
 tests/lean/interactive/run.lean | 45 +++++++++++++++++++++++++--------
 1 file changed, 35 insertions(+), 10 deletions(-)

diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index 794ce80fcc..504cf3c74f 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -15,24 +15,49 @@ def main (args : List String) : IO Unit := do
     let _ ← Ipc.collectDiagnostics 1 uri 1
     let mut lineNo := 0
     let mut lastActualLineNo := 0
+    let mut versionNo : Nat := 2
     let mut requestNo : Nat := 2
     for line in text.splitOn "\n" do
       match line.splitOn "--^" with
       | [ws, directive] =>
         let colon := directive.posOf ':'
         let method := directive.extract 0 colon |>.trim
-        let params := if colon < directive.bsize then directive.extract (colon + 1) directive.bsize |>.trim else "{}"
-        let Except.ok params ← pure <| Json.parse params
-          | throw <| IO.userError s!"failed to parse {params}"
-        let params := params.setObjVal! "textDocument" (toJson { uri := uri : TextDocumentIdentifier })
         -- TODO: correctly compute in presence of Unicode
         let column := ws.bsize + "--".length
-        let params := params.setObjVal! "position" (toJson { line := lastActualLineNo, character := column : Lsp.Position })
-        IO.eprintln params
-        Ipc.writeRequest ⟨requestNo, method, params⟩
-        let resp ← Ipc.readResponseAs requestNo Json
-        IO.eprintln resp.result
-        requestNo := requestNo + 1
+        let pos : Lsp.Position := { line := lastActualLineNo, character := column }
+        let params := if colon < directive.bsize then directive.extract (colon + 1) directive.bsize |>.trim else "{}"
+        match method with
+        | "insert" =>
+          let params : DidChangeTextDocumentParams := {
+            textDocument := {
+              uri      := uri
+              version? := versionNo
+            }
+            contentChanges := #[TextDocumentContentChangeEvent.rangeChange {
+              start := pos
+              «end» := { pos with character := pos.character + params.bsize }
+            } params]
+          }
+          let params := toJson params
+          IO.eprintln params
+          Ipc.writeNotification ⟨"textDocument/didChange", params⟩
+          let diags ← Ipc.collectDiagnostics requestNo uri versionNo
+          --for diag in diags do
+          --  IO.eprintln (toJson diag.param)
+          requestNo := requestNo + 1
+          versionNo := versionNo + 1
+        | _ =>
+          let Except.ok params ← pure <| Json.parse params
+            | throw <| IO.userError s!"failed to parse {params}"
+          let params := params.setObjVal! "textDocument" (toJson { uri := uri : TextDocumentIdentifier })
+          -- TODO: correctly compute in presence of Unicode
+          let column := ws.bsize + "--".length
+          let params := params.setObjVal! "position" (toJson pos)
+          IO.eprintln params
+          Ipc.writeRequest ⟨requestNo, method, params⟩
+          let resp ← Ipc.readResponseAs requestNo Json
+          IO.eprintln resp.result
+          requestNo := requestNo + 1
       | _ =>
         lastActualLineNo := lineNo
       lineNo := lineNo + 1