test: dot completion

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

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}

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