From f4c5f8e422ac3edbcc6ac6f00791b730ea258f3f Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Fri, 6 Feb 2026 09:57:27 +0100 Subject: [PATCH] fix: set `data?` field in eager code actions (#12332) This PR fixes an issue on new NeoVim versions that would cause the language server to display an error when using certain code actions. (For some reason, NeoVim recently decided to diverge from VS Code in terms of when it emits code action resolution requests, which means that not setting the `data?` field won't preclude NeoVim from emitting a request anymore, which in turn means that the server can't resolve the code action.) --- src/Lean/Server/CodeActions/Basic.lean | 4 +- .../builtinCodeactions.lean.expected.out | 34 +- .../interactive/codeActions.lean.expected.out | 152 ++- .../interactive/codeaction.lean.expected.out | 30 +- .../structInstFieldHints.lean.expected.out | 1205 ++++++++++++++++- .../terminationBySuggestion.lean.expected.out | 164 ++- .../tryThisCodeAction.lean.expected.out | 32 +- 7 files changed, 1570 insertions(+), 51 deletions(-) diff --git a/src/Lean/Server/CodeActions/Basic.lean b/src/Lean/Server/CodeActions/Basic.lean index 7107fbc766..6d73b6b61d 100644 --- a/src/Lean/Server/CodeActions/Basic.lean +++ b/src/Lean/Server/CodeActions/Basic.lean @@ -134,7 +134,6 @@ def handleCodeAction (params : CodeActionParams) : RequestM (RequestTask (Array RequestM.checkCancelled let cas ← cap params snap cas.mapIdxM fun i lca => do - if lca.lazy?.isNone then return lca.eager let data : CodeActionResolveData := { params, providerName, providerResultIndex := i } @@ -165,7 +164,8 @@ def handleCodeActionResolve (param : CodeAction) : RequestM (RequestTask CodeAct let some ca := cas[data.providerResultIndex]? | throw <| RequestError.internalError s!"Failed to resolve code action index {data.providerResultIndex}." let some lazy := ca.lazy? - | throw <| RequestError.internalError s!"Can't resolve; nothing further to resolve." + -- Eager code action - return unchanged + | return param let r ← liftM lazy return r diff --git a/tests/lean/interactive/builtinCodeactions.lean.expected.out b/tests/lean/interactive/builtinCodeactions.lean.expected.out index 3a2d20f486..9e2d61ef55 100644 --- a/tests/lean/interactive/builtinCodeactions.lean.expected.out +++ b/tests/lean/interactive/builtinCodeactions.lean.expected.out @@ -13,4 +13,36 @@ {"start": {"line": 5, "character": 2}, "end": {"line": 5, "character": 97}}, "newText": - "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}}] + "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///builtinCodeactions.lean"}, + "range": + {"start": {"line": 5, "character": 4}, "end": {"line": 5, "character": 4}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, + aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h: +{"title": + "Try this: simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///builtinCodeactions.lean"}, + "edits": + [{"range": + {"start": {"line": 5, "character": 2}, + "end": {"line": 5, "character": 97}}, + "newText": + "simp only [AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,\n aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] at h"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///builtinCodeactions.lean"}, + "range": + {"start": {"line": 5, "character": 4}, "end": {"line": 5, "character": 4}}, + "context": {"diagnostics": []}}}} diff --git a/tests/lean/interactive/codeActions.lean.expected.out b/tests/lean/interactive/codeActions.lean.expected.out index 682b20cc96..b3fb149c88 100644 --- a/tests/lean/interactive/codeActions.lean.expected.out +++ b/tests/lean/interactive/codeActions.lean.expected.out @@ -11,7 +11,35 @@ [{"range": {"start": {"line": 56, "character": 0}, "end": {"line": 56, "character": 16}}, - "newText": "foo"}]}]}}] + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 56, "character": 4}, + "end": {"line": 56, "character": 4}}, + "context": {"diagnostics": []}}}}] +Resolution of foo: +{"title": "foo", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"}, + "edits": + [{"range": + {"start": {"line": 56, "character": 0}, + "end": {"line": 56, "character": 16}}, + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 56, "character": 4}, "end": {"line": 56, "character": 4}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///codeActions.lean"}, "range": {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}}, @@ -25,7 +53,16 @@ [{"range": {"start": {"line": 59, "character": 0}, "end": {"line": 59, "character": 4}}, - "newText": "#eval 0"}]}]}}, + "newText": "#eval 0"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.cmdCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 59, "character": 2}, + "end": {"line": 59, "character": 2}}, + "context": {"diagnostics": []}}}}, {"title": "foo", "kind": "quickfix", "edit": @@ -35,7 +72,54 @@ [{"range": {"start": {"line": 59, "character": 0}, "end": {"line": 59, "character": 4}}, - "newText": "foo"}]}]}}] + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 59, "character": 2}, + "end": {"line": 59, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of bar: +{"title": "bar", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"}, + "edits": + [{"range": + {"start": {"line": 59, "character": 0}, + "end": {"line": 59, "character": 4}}, + "newText": "#eval 0"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.cmdCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}}, + "context": {"diagnostics": []}}}} +Resolution of foo: +{"title": "foo", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"}, + "edits": + [{"range": + {"start": {"line": 59, "character": 0}, + "end": {"line": 59, "character": 4}}, + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 59, "character": 2}, "end": {"line": 59, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///codeActions.lean"}, "range": {"start": {"line": 62, "character": 18}, "end": {"line": 62, "character": 18}}, @@ -49,7 +133,16 @@ [{"range": {"start": {"line": 62, "character": 17}, "end": {"line": 62, "character": 18}}, - "newText": "\"foobar\""}]}]}}, + "newText": "\"foobar\""}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.holeCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 62, "character": 18}, + "end": {"line": 62, "character": 18}}, + "context": {"diagnostics": []}}}}, {"title": "foo", "kind": "quickfix", "edit": @@ -59,4 +152,53 @@ [{"range": {"start": {"line": 62, "character": 0}, "end": {"line": 62, "character": 18}}, - "newText": "foo"}]}]}}] + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 62, "character": 18}, + "end": {"line": 62, "character": 18}}, + "context": {"diagnostics": []}}}}] +Resolution of foobar: +{"title": "foobar", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"}, + "edits": + [{"range": + {"start": {"line": 62, "character": 17}, + "end": {"line": 62, "character": 18}}, + "newText": "\"foobar\""}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "Lean.CodeAction.holeCodeActionProvider", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 62, "character": 18}, + "end": {"line": 62, "character": 18}}, + "context": {"diagnostics": []}}}} +Resolution of foo: +{"title": "foo", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeActions.lean"}, + "edits": + [{"range": + {"start": {"line": 62, "character": 0}, + "end": {"line": 62, "character": 18}}, + "newText": "foo"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "foo", + "params": + {"textDocument": {"uri": "file:///codeActions.lean"}, + "range": + {"start": {"line": 62, "character": 18}, + "end": {"line": 62, "character": 18}}, + "context": {"diagnostics": []}}}} diff --git a/tests/lean/interactive/codeaction.lean.expected.out b/tests/lean/interactive/codeaction.lean.expected.out index 71df19d8c4..843c5c521c 100644 --- a/tests/lean/interactive/codeaction.lean.expected.out +++ b/tests/lean/interactive/codeaction.lean.expected.out @@ -11,7 +11,16 @@ [{"range": {"start": {"line": 28, "character": 4}, "end": {"line": 28, "character": 4}}, - "newText": "hello!!!"}]}]}}, + "newText": "hello!!!"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "helloProvider", + "params": + {"textDocument": {"uri": "file:///codeaction.lean"}, + "range": + {"start": {"line": 28, "character": 4}, + "end": {"line": 28, "character": 4}}, + "context": {"diagnostics": []}}}}, {"title": "a long-running action", "kind": "refactor", "data": @@ -23,6 +32,25 @@ {"start": {"line": 28, "character": 4}, "end": {"line": 28, "character": 4}}, "context": {"diagnostics": []}}}}] +Resolution of hello world: +{"title": "hello world", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///codeaction.lean"}, + "edits": + [{"range": + {"start": {"line": 28, "character": 4}, + "end": {"line": 28, "character": 4}}, + "newText": "hello!!!"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": "helloProvider", + "params": + {"textDocument": {"uri": "file:///codeaction.lean"}, + "range": + {"start": {"line": 28, "character": 4}, "end": {"line": 28, "character": 4}}, + "context": {"diagnostics": []}}}} Resolution of a long-running action: {"title": "a long-running action", "kind": "refactor", diff --git a/tests/lean/interactive/structInstFieldHints.lean.expected.out b/tests/lean/interactive/structInstFieldHints.lean.expected.out index a1ed80cc29..c40a233cf7 100644 --- a/tests/lean/interactive/structInstFieldHints.lean.expected.out +++ b/tests/lean/interactive/structInstFieldHints.lean.expected.out @@ -12,7 +12,38 @@ {"start": {"line": 20, "character": 3}, "end": {"line": 20, "character": 3}}, "newText": - " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}}] + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 20, "character": 2}, + "end": {"line": 20, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 20, "character": 3}, + "end": {"line": 20, "character": 3}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 20, "character": 2}, "end": {"line": 20, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 22, "character": 15}, "end": {"line": 22, "character": 15}}, @@ -27,7 +58,39 @@ {"start": {"line": 22, "character": 16}, "end": {"line": 22, "character": 16}}, "newText": - " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}}] + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 22, "character": 15}, + "end": {"line": 22, "character": 15}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 22, "character": 16}, + "end": {"line": 22, "character": 16}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 22, "character": 15}, + "end": {"line": 22, "character": 15}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 27, "character": 2}, "end": {"line": 27, "character": 2}}, @@ -42,7 +105,38 @@ {"start": {"line": 26, "character": 0}, "end": {"line": 26, "character": 0}}, "newText": - " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 27, "character": 2}, + "end": {"line": 27, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 26, "character": 0}, + "end": {"line": 26, "character": 0}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 27, "character": 2}, "end": {"line": 27, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 2}}, @@ -57,7 +151,38 @@ {"start": {"line": 31, "character": 0}, "end": {"line": 31, "character": 0}}, "newText": - " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 32, "character": 2}, + "end": {"line": 32, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 31, "character": 0}, + "end": {"line": 31, "character": 0}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 32, "character": 2}, "end": {"line": 32, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 37, "character": 2}, "end": {"line": 37, "character": 2}}, @@ -72,7 +197,38 @@ {"start": {"line": 36, "character": 3}, "end": {"line": 36, "character": 3}}, "newText": - "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 37, "character": 2}, + "end": {"line": 37, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 36, "character": 3}, + "end": {"line": 36, "character": 3}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 37, "character": 2}, "end": {"line": 37, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 40, "character": 2}, "end": {"line": 40, "character": 2}}, @@ -87,7 +243,38 @@ {"start": {"line": 39, "character": 16}, "end": {"line": 39, "character": 16}}, "newText": - "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 40, "character": 2}, + "end": {"line": 40, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 39, "character": 16}, + "end": {"line": 39, "character": 16}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 40, "character": 2}, "end": {"line": 40, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 2}}, @@ -102,7 +289,38 @@ {"start": {"line": 42, "character": 16}, "end": {"line": 42, "character": 16}}, "newText": - "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 44, "character": 2}, + "end": {"line": 44, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 42, "character": 16}, + "end": {"line": 42, "character": 16}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 50, "character": 17}, "end": {"line": 50, "character": 17}}, @@ -117,7 +335,39 @@ {"start": {"line": 50, "character": 18}, "end": {"line": 50, "character": 18}}, "newText": - "\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 50, "character": 17}, + "end": {"line": 50, "character": 17}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 50, "character": 18}, + "end": {"line": 50, "character": 18}}, + "newText": + "\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 50, "character": 17}, + "end": {"line": 50, "character": 17}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 58, "character": 2}, "end": {"line": 58, "character": 2}}, @@ -132,7 +382,38 @@ {"start": {"line": 57, "character": 18}, "end": {"line": 57, "character": 18}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 58, "character": 2}, + "end": {"line": 58, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 57, "character": 18}, + "end": {"line": 57, "character": 18}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 58, "character": 2}, "end": {"line": 58, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 2}}, @@ -146,7 +427,37 @@ [{"range": {"start": {"line": 64, "character": 16}, "end": {"line": 64, "character": 16}}, - "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}}] + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 65, "character": 2}, + "end": {"line": 65, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 64, "character": 16}, + "end": {"line": 64, "character": 16}}, + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 70, "character": 30}, "end": {"line": 70, "character": 30}}, @@ -160,7 +471,38 @@ [{"range": {"start": {"line": 70, "character": 31}, "end": {"line": 70, "character": 31}}, - "newText": ", sh := _, longerFieldName := _, field3 := _"}]}]}}] + "newText": ", sh := _, longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 70, "character": 30}, + "end": {"line": 70, "character": 30}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 70, "character": 31}, + "end": {"line": 70, "character": 31}}, + "newText": ", sh := _, longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 70, "character": 30}, + "end": {"line": 70, "character": 30}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 75, "character": 94}, "end": {"line": 75, "character": 94}}, @@ -174,7 +516,38 @@ [{"range": {"start": {"line": 75, "character": 95}, "end": {"line": 75, "character": 95}}, - "newText": ",\n field2 := _, longerFieldName := _, field3 := _"}]}]}}] + "newText": ",\n field2 := _, longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 75, "character": 94}, + "end": {"line": 75, "character": 94}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 75, "character": 95}, + "end": {"line": 75, "character": 95}}, + "newText": ",\n field2 := _, longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 75, "character": 94}, + "end": {"line": 75, "character": 94}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 81, "character": 17}, "end": {"line": 81, "character": 17}}, @@ -188,7 +561,38 @@ [{"range": {"start": {"line": 81, "character": 18}, "end": {"line": 81, "character": 18}}, - "newText": ", longerFieldName := _, field3 := _"}]}]}}] + "newText": ", longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 81, "character": 17}, + "end": {"line": 81, "character": 17}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 81, "character": 18}, + "end": {"line": 81, "character": 18}}, + "newText": ", longerFieldName := _, field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 81, "character": 17}, + "end": {"line": 81, "character": 17}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 86, "character": 13}, "end": {"line": 86, "character": 13}}, @@ -203,7 +607,39 @@ {"start": {"line": 86, "character": 14}, "end": {"line": 86, "character": 14}}, "newText": - "\n field1 := _\n field2 := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 86, "character": 13}, + "end": {"line": 86, "character": 13}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 86, "character": 14}, + "end": {"line": 86, "character": 14}}, + "newText": + "\n field1 := _\n field2 := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 86, "character": 13}, + "end": {"line": 86, "character": 13}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 94, "character": 40}, "end": {"line": 94, "character": 40}}, @@ -217,7 +653,38 @@ [{"range": {"start": {"line": 94, "character": 41}, "end": {"line": 94, "character": 41}}, - "newText": ", field2 := _, longerFieldName := _"}]}]}}] + "newText": ", field2 := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 94, "character": 40}, + "end": {"line": 94, "character": 40}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 94, "character": 41}, + "end": {"line": 94, "character": 41}}, + "newText": ", field2 := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 94, "character": 40}, + "end": {"line": 94, "character": 40}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 99, "character": 95}, "end": {"line": 99, "character": 95}}, @@ -231,7 +698,38 @@ [{"range": {"start": {"line": 99, "character": 96}, "end": {"line": 99, "character": 96}}, - "newText": ",\n field2 := _, longerFieldName := _"}]}]}}] + "newText": ",\n field2 := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 99, "character": 95}, + "end": {"line": 99, "character": 95}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 99, "character": 96}, + "end": {"line": 99, "character": 96}}, + "newText": ",\n field2 := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 99, "character": 95}, + "end": {"line": 99, "character": 95}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 106, "character": 2}, "end": {"line": 106, "character": 2}}, @@ -245,7 +743,38 @@ [{"range": {"start": {"line": 105, "character": 16}, "end": {"line": 105, "character": 16}}, - "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}}] + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 106, "character": 2}, + "end": {"line": 106, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 105, "character": 16}, + "end": {"line": 105, "character": 16}}, + "newText": "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 106, "character": 2}, + "end": {"line": 106, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 112, "character": 27}, @@ -261,7 +790,39 @@ {"start": {"line": 112, "character": 28}, "end": {"line": 112, "character": 28}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 112, "character": 27}, + "end": {"line": 112, "character": 27}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 112, "character": 28}, + "end": {"line": 112, "character": 28}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 112, "character": 27}, + "end": {"line": 112, "character": 27}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 117, "character": 12}, @@ -277,7 +838,39 @@ {"start": {"line": 117, "character": 13}, "end": {"line": 117, "character": 13}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 117, "character": 12}, + "end": {"line": 117, "character": 12}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 117, "character": 13}, + "end": {"line": 117, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 117, "character": 12}, + "end": {"line": 117, "character": 12}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 121, "character": 2}, "end": {"line": 121, "character": 2}}, @@ -292,7 +885,39 @@ {"start": {"line": 120, "character": 13}, "end": {"line": 120, "character": 13}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 121, "character": 2}, + "end": {"line": 121, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 120, "character": 13}, + "end": {"line": 120, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 121, "character": 2}, + "end": {"line": 121, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 124, "character": 2}, "end": {"line": 124, "character": 2}}, @@ -307,7 +932,39 @@ {"start": {"line": 123, "character": 26}, "end": {"line": 123, "character": 26}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 124, "character": 2}, + "end": {"line": 124, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 123, "character": 26}, + "end": {"line": 123, "character": 26}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 124, "character": 2}, + "end": {"line": 124, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 128, "character": 2}, "end": {"line": 128, "character": 2}}, @@ -322,7 +979,39 @@ {"start": {"line": 127, "character": 0}, "end": {"line": 127, "character": 0}}, "newText": - " field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + " field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 128, "character": 2}, + "end": {"line": 128, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 127, "character": 0}, + "end": {"line": 127, "character": 0}}, + "newText": + " field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 128, "character": 2}, + "end": {"line": 128, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 136, "character": 2}, "end": {"line": 136, "character": 2}}, @@ -336,7 +1025,38 @@ [{"range": {"start": {"line": 135, "character": 16}, "end": {"line": 135, "character": 16}}, - "newText": ", sh := _, longerFieldName := _"}]}]}}] + "newText": ", sh := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 136, "character": 2}, + "end": {"line": 136, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 135, "character": 16}, + "end": {"line": 135, "character": 16}}, + "newText": ", sh := _, longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 136, "character": 2}, + "end": {"line": 136, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 142, "character": 2}, "end": {"line": 142, "character": 2}}, @@ -351,7 +1071,39 @@ {"start": {"line": 140, "character": 12}, "end": {"line": 140, "character": 12}}, "newText": - "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 142, "character": 2}, + "end": {"line": 142, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 140, "character": 12}, + "end": {"line": 140, "character": 12}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 142, "character": 2}, + "end": {"line": 142, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 144, "character": 12}, @@ -367,7 +1119,39 @@ {"start": {"line": 144, "character": 12}, "end": {"line": 144, "character": 12}}, "newText": - " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}}] + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 144, "character": 12}, + "end": {"line": 144, "character": 12}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 144, "character": 12}, + "end": {"line": 144, "character": 12}}, + "newText": + " field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 144, "character": 12}, + "end": {"line": 144, "character": 12}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 147, "character": 2}, "end": {"line": 147, "character": 2}}, @@ -382,7 +1166,39 @@ {"start": {"line": 146, "character": 12}, "end": {"line": 146, "character": 12}}, "newText": - "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 147, "character": 2}, + "end": {"line": 147, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 146, "character": 12}, + "end": {"line": 146, "character": 12}}, + "newText": + "\n field1 := _\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 147, "character": 2}, + "end": {"line": 147, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 152, "character": 2}, "end": {"line": 152, "character": 2}}, @@ -397,7 +1213,39 @@ {"start": {"line": 150, "character": 13}, "end": {"line": 150, "character": 13}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 152, "character": 2}, + "end": {"line": 152, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 150, "character": 13}, + "end": {"line": 150, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 152, "character": 2}, + "end": {"line": 152, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 156, "character": 17}, @@ -413,7 +1261,39 @@ {"start": {"line": 156, "character": 18}, "end": {"line": 156, "character": 18}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 156, "character": 17}, + "end": {"line": 156, "character": 17}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 156, "character": 18}, + "end": {"line": 156, "character": 18}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 156, "character": 17}, + "end": {"line": 156, "character": 17}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 158, "character": 23}, @@ -429,7 +1309,39 @@ {"start": {"line": 158, "character": 24}, "end": {"line": 158, "character": 24}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 158, "character": 23}, + "end": {"line": 158, "character": 23}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 158, "character": 24}, + "end": {"line": 158, "character": 24}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 158, "character": 23}, + "end": {"line": 158, "character": 23}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 163, "character": 12}, @@ -445,7 +1357,39 @@ {"start": {"line": 163, "character": 13}, "end": {"line": 163, "character": 13}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 163, "character": 12}, + "end": {"line": 163, "character": 12}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 163, "character": 13}, + "end": {"line": 163, "character": 13}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 163, "character": 12}, + "end": {"line": 163, "character": 12}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 167, "character": 2}, "end": {"line": 167, "character": 2}}, @@ -460,7 +1404,39 @@ {"start": {"line": 165, "character": 22}, "end": {"line": 165, "character": 22}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 167, "character": 2}, + "end": {"line": 167, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 165, "character": 22}, + "end": {"line": 165, "character": 22}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 167, "character": 2}, + "end": {"line": 167, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 171, "character": 2}, "end": {"line": 171, "character": 2}}, @@ -475,7 +1451,39 @@ {"start": {"line": 169, "character": 22}, "end": {"line": 169, "character": 22}}, "newText": - "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 171, "character": 2}, + "end": {"line": 171, "character": 2}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 169, "character": 22}, + "end": {"line": 169, "character": 22}}, + "newText": + "\n field2 := _\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 171, "character": 2}, + "end": {"line": 171, "character": 2}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 176, "character": 17}, @@ -491,7 +1499,39 @@ {"start": {"line": 176, "character": 18}, "end": {"line": 176, "character": 18}}, "newText": - "\n field1 := 0\n sh := _\n longerFieldName := _\n field3 := _"}]}]}}] + "\n field1 := 0\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 176, "character": 17}, + "end": {"line": 176, "character": 17}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 176, "character": 18}, + "end": {"line": 176, "character": 18}}, + "newText": + "\n field1 := 0\n sh := _\n longerFieldName := _\n field3 := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 176, "character": 17}, + "end": {"line": 176, "character": 17}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 186, "character": 13}, @@ -506,7 +1546,38 @@ [{"range": {"start": {"line": 186, "character": 14}, "end": {"line": 186, "character": 14}}, - "newText": "\n n := ?_ + 4"}]}]}}] + "newText": "\n n := ?_ + 4"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 186, "character": 13}, + "end": {"line": 186, "character": 13}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 186, "character": 14}, + "end": {"line": 186, "character": 14}}, + "newText": "\n n := ?_ + 4"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 186, "character": 13}, + "end": {"line": 186, "character": 13}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 190, "character": 27}, @@ -521,7 +1592,38 @@ [{"range": {"start": {"line": 190, "character": 28}, "end": {"line": 190, "character": 28}}, - "newText": " fst := _\n snd := _ "}]}]}}] + "newText": " fst := _\n snd := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 190, "character": 27}, + "end": {"line": 190, "character": 27}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 190, "character": 28}, + "end": {"line": 190, "character": 28}}, + "newText": " fst := _\n snd := _ "}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 190, "character": 27}, + "end": {"line": 190, "character": 27}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 192, "character": 38}, @@ -536,7 +1638,38 @@ [{"range": {"start": {"line": 192, "character": 39}, "end": {"line": 192, "character": 39}}, - "newText": "\n snd := _"}]}]}}] + "newText": "\n snd := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 192, "character": 38}, + "end": {"line": 192, "character": 38}}, + "context": {"diagnostics": []}}}}] +Resolution of Add missing fields: +{"title": "Add missing fields", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///structInstFieldHints.lean"}, + "edits": + [{"range": + {"start": {"line": 192, "character": 39}, + "end": {"line": 192, "character": 39}}, + "newText": "\n snd := _"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, + "range": + {"start": {"line": 192, "character": 38}, + "end": {"line": 192, "character": 38}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///structInstFieldHints.lean"}, "range": {"start": {"line": 199, "character": 16}, diff --git a/tests/lean/interactive/terminationBySuggestion.lean.expected.out b/tests/lean/interactive/terminationBySuggestion.lean.expected.out index 8a0b40ac01..8233d08de5 100644 --- a/tests/lean/interactive/terminationBySuggestion.lean.expected.out +++ b/tests/lean/interactive/terminationBySuggestion.lean.expected.out @@ -12,7 +12,37 @@ [{"range": {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 15}}, - "newText": "termination_by (n, m)"}]}]}}] + "newText": "termination_by (n, m)"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 4, "character": 5}, "end": {"line": 4, "character": 5}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: termination_by (n, m): +{"title": "Try this: termination_by (n, m)", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 4, "character": 0}, + "end": {"line": 4, "character": 15}}, + "newText": "termination_by (n, m)"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 4, "character": 5}, "end": {"line": 4, "character": 5}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, "range": {"start": {"line": 11, "character": 5}, "end": {"line": 11, "character": 5}}, @@ -27,7 +57,38 @@ [{"range": {"start": {"line": 11, "character": 0}, "end": {"line": 11, "character": 15}}, - "newText": "termination_by structural n"}]}]}}] + "newText": "termination_by structural n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 11, "character": 5}, + "end": {"line": 11, "character": 5}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: termination_by structural n: +{"title": "Try this: termination_by structural n", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 11, "character": 0}, + "end": {"line": 11, "character": 15}}, + "newText": "termination_by structural n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 11, "character": 5}, "end": {"line": 11, "character": 5}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, "range": {"start": {"line": 17, "character": 5}, "end": {"line": 17, "character": 5}}, @@ -42,7 +103,38 @@ [{"range": {"start": {"line": 17, "character": 0}, "end": {"line": 17, "character": 15}}, - "newText": "termination_by structural x => x"}]}]}}] + "newText": "termination_by structural x => x"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 17, "character": 5}, + "end": {"line": 17, "character": 5}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: termination_by structural x => x: +{"title": "Try this: termination_by structural x => x", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 17, "character": 0}, + "end": {"line": 17, "character": 15}}, + "newText": "termination_by structural x => x"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 17, "character": 5}, "end": {"line": 17, "character": 5}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, "range": {"start": {"line": 24, "character": 5}, "end": {"line": 24, "character": 5}}, @@ -57,7 +149,38 @@ [{"range": {"start": {"line": 24, "character": 0}, "end": {"line": 24, "character": 15}}, - "newText": "termination_by n"}]}]}}] + "newText": "termination_by n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 24, "character": 5}, + "end": {"line": 24, "character": 5}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: termination_by n: +{"title": "Try this: termination_by n", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 24, "character": 0}, + "end": {"line": 24, "character": 15}}, + "newText": "termination_by n"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 24, "character": 5}, "end": {"line": 24, "character": 5}}, + "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, "range": {"start": {"line": 31, "character": 5}, "end": {"line": 31, "character": 5}}, @@ -72,4 +195,35 @@ [{"range": {"start": {"line": 31, "character": 0}, "end": {"line": 31, "character": 15}}, - "newText": "termination_by x1 => x1"}]}]}}] + "newText": "termination_by x1 => x1"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 31, "character": 5}, + "end": {"line": 31, "character": 5}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: termination_by x1 => x1: +{"title": "Try this: termination_by x1 => x1", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": + {"version": 1, "uri": "file:///terminationBySuggestion.lean"}, + "edits": + [{"range": + {"start": {"line": 31, "character": 0}, + "end": {"line": 31, "character": 15}}, + "newText": "termination_by x1 => x1"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///terminationBySuggestion.lean"}, + "range": + {"start": {"line": 31, "character": 5}, "end": {"line": 31, "character": 5}}, + "context": {"diagnostics": []}}}} diff --git a/tests/lean/interactive/tryThisCodeAction.lean.expected.out b/tests/lean/interactive/tryThisCodeAction.lean.expected.out index b8759acd23..95e764ad34 100644 --- a/tests/lean/interactive/tryThisCodeAction.lean.expected.out +++ b/tests/lean/interactive/tryThisCodeAction.lean.expected.out @@ -11,4 +11,34 @@ [{"range": {"start": {"line": 0, "character": 21}, "end": {"line": 0, "character": 26}}, - "newText": "simp only"}]}]}}] + "newText": "simp only"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///tryThisCodeAction.lean"}, + "range": + {"start": {"line": 0, "character": 22}, + "end": {"line": 0, "character": 22}}, + "context": {"diagnostics": []}}}}] +Resolution of Try this: simp only: +{"title": "Try this: simp only", + "kind": "quickfix", + "edit": + {"documentChanges": + [{"textDocument": {"version": 1, "uri": "file:///tryThisCodeAction.lean"}, + "edits": + [{"range": + {"start": {"line": 0, "character": 21}, + "end": {"line": 0, "character": 26}}, + "newText": "simp only"}]}]}, + "data": + {"providerResultIndex": 0, + "providerName": + "_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.tryThisProvider", + "params": + {"textDocument": {"uri": "file:///tryThisCodeAction.lean"}, + "range": + {"start": {"line": 0, "character": 22}, "end": {"line": 0, "character": 22}}, + "context": {"diagnostics": []}}}}