From 46be48211e8c115a37c7fbb65c2889221b19df92 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 5 Apr 2021 13:59:50 +0200
Subject: [PATCH] test: dot completion

---
 tests/lean/interactive/completion.lean        | 17 +++++++++++++
 .../interactive/completion.lean.expected.out  | 24 +++++++++++++++++++
 tests/lean/interactive/run.lean               |  7 ++++--
 3 files changed, 46 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/interactive/completion.lean
 create mode 100644 tests/lean/interactive/completion.lean.expected.out

diff --git a/tests/lean/interactive/completion.lean b/tests/lean/interactive/completion.lean
new file mode 100644
index 0000000000..defab7a739
--- /dev/null
+++ b/tests/lean/interactive/completion.lean
@@ -0,0 +1,17 @@
+structure Foo where
+  foo : Nat
+
+example (f : Foo) : f.
+                    --^ textDocument/completion
+example : Nat := 0  -- recover
+
+example (f : Foo) : f.f
+                     --^ textDocument/completion
+example : Nat := 0  -- recover
+
+example (f : Foo) : id f |>.
+                          --^ textDocument/completion
+example : Nat := 0  -- recover
+
+example (f : Foo) : id f |>.f
+                           --^ textDocument/completion
diff --git a/tests/lean/interactive/completion.lean.expected.out b/tests/lean/interactive/completion.lean.expected.out
new file mode 100644
index 0000000000..bc5c33e059
--- /dev/null
+++ b/tests/lean/interactive/completion.lean.expected.out
@@ -0,0 +1,24 @@
+{"textDocument": {"uri": "file://completion.lean"},
+ "position": {"line": 3, "character": 22}}
+{"items":
+ [{"label": "foo", "detail": "Foo → Nat"},
+  {"label": "mk", "detail": "Nat → Foo"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion.lean"},
+ "position": {"line": 7, "character": 23}}
+{"items":
+ [{"label": "foo", "detail": "Foo → Nat"},
+  {"label": "mk", "detail": "Nat → Foo"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion.lean"},
+ "position": {"line": 11, "character": 28}}
+{"items":
+ [{"label": "foo", "detail": "Foo → Nat"},
+  {"label": "mk", "detail": "Nat → Foo"}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file://completion.lean"},
+ "position": {"line": 15, "character": 29}}
+{"items":
+ [{"label": "foo", "detail": "Foo → Nat"},
+  {"label": "mk", "detail": "Nat → Foo"}],
+ "isIncomplete": true}
diff --git a/tests/lean/interactive/run.lean b/tests/lean/interactive/run.lean
index 3d8464bd78..794ce80fcc 100644
--- a/tests/lean/interactive/run.lean
+++ b/tests/lean/interactive/run.lean
@@ -14,6 +14,7 @@ def main (args : List String) : IO Unit := do
       textDocument := { uri := uri, languageId := "lean", version := 1, text := text } : DidOpenTextDocumentParams }⟩
     let _ ← Ipc.collectDiagnostics 1 uri 1
     let mut lineNo := 0
+    let mut lastActualLineNo := 0
     let mut requestNo : Nat := 2
     for line in text.splitOn "\n" do
       match line.splitOn "--^" with
@@ -26,13 +27,15 @@ def main (args : List String) : IO Unit := do
         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 := lineNo - 1, character := column : Lsp.Position })
+        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
-      | _ => lineNo := lineNo + 1
+      | _ =>
+        lastActualLineNo := lineNo
+      lineNo := lineNo + 1
     Ipc.writeRequest ⟨requestNo, "shutdown", Json.null⟩
     let shutResp ← Ipc.readResponseAs requestNo Json
     assert! shutResp.result.isNull