chore: add code action test back in (#9669)

This PR re-adds the code action test that was reverted in
5b18ea1545, now with more robustness.
This commit is contained in:
Kyle Miller 2025-08-01 11:41:41 -07:00 committed by GitHub
parent 2ea6b5068c
commit 08ff19d973
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 56 additions and 0 deletions

View file

@ -66,3 +66,17 @@ example : MyNat → MyNat := .succ
--^ textDocument/completion
open MyLib in
example : MyNat → MyNat := .succ' -- it successfully elaborates
/-!
The missing import code action works.
-/
--^ waitForILeans
example : IO.FS.Stream := .chainLef
--^ codeAction
example : outParam IO.FS.Stream := .chainLef
--^ codeAction
example : Nat → IO.FS.Stream := .chainLef
--^ codeAction

View file

@ -85,3 +85,45 @@
"id": {"const": {"declName": "MyNat.succ"}},
"cPos": 0}}],
"isIncomplete": false}
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Utils\n"},
{"range":
{"start": {"line": 74, "character": 27},
"end": {"line": 74, "character": 35}},
"newText": "chainLeft"}]}]}}
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Utils\n"},
{"range":
{"start": {"line": 77, "character": 36},
"end": {"line": 77, "character": 44}},
"newText": "chainLeft"}]}]}}
{"title": "Import IO.FS.Stream.chainLeft from Lean.Server.Utils",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument": {"version": 1, "uri": "file:///dottedIdentNotation.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Utils\n"},
{"range":
{"start": {"line": 80, "character": 33},
"end": {"line": 80, "character": 41}},
"newText": "chainLeft"}]}]}}