max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out
Marc Huisinga 4329eae8d4
fix: unknown identifier minimization (#10797) 
This PR fixes a bug in the unknown identifier code actions where the
identifiers wouldn't be correctly minimized in nested namespaces. It
also fixes a bug where identifiers would sometimes be minimized to
`[anonymous]`.

The first bug was introduced in #10619.
2025-10-15 19:25:27 +00:00

483 lines
18 KiB
Text
Raw Blame History

{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 1, "character": 34}, "end": {"line": 1, "character": 34}},
"context": {"diagnostics": []}}
[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 1, "character": 7},
"end": {"line": 1, "character": 34}},
"newText": "Lean.Server.Test.Refs.Test1"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 1, "character": 7},
"end": {"line": 1, "character": 34}},
"newText": "Lean.Server.Test.Refs.test10"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 4, "character": 33}, "end": {"line": 4, "character": 33}},
"context": {"diagnostics": []}}
[{"title": "Import LeanServerTestRefsTest0 from Lean.Server.Test.Refs",
"kind": "refactor",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 4, "character": 10},
"end": {"line": 4, "character": 33}},
"newText": "LeanServerTestRefsTest0"}]}]}},
{"title":
"Import Lean.Server.Test.LeanServerTestRefsTest0' from Lean.Server.Test.Refs",
"kind": "refactor",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 4, "character": 10},
"end": {"line": 4, "character": 33}},
"newText": "Lean.Server.Test.LeanServerTestRefsTest0'"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
"kind": "refactor",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 4, "character": 10},
"end": {"line": 4, "character": 33}},
"newText": "Lean.Server.Test.Refs.test10"}]}]}},
{"title": "Import all unambiguous unknown identifiers",
"kind": "quickfix",
"data":
{"providerResultIndex": 0,
"providerName": "unknownIdentifiers",
"params":
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 4, "character": 33},
"end": {"line": 4, "character": 33}},
"context": {"diagnostics": []}}}}]
Resolution of Import all unambiguous unknown identifiers:
{"title": "Import all unambiguous unknown identifiers",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 13, "character": 7},
"end": {"line": 13, "character": 48}},
"newText": "LeanServerTestRefsTest0'"},
{"range":
{"start": {"line": 24, "character": 7},
"end": {"line": 24, "character": 34}},
"newText": "Test1"},
{"range":
{"start": {"line": 4, "character": 10},
"end": {"line": 4, "character": 33}},
"newText": "LeanServerTestRefsTest0"}]}]},
"data":
{"providerResultIndex": 0,
"providerName": "unknownIdentifiers",
"params":
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 4, "character": 33}, "end": {"line": 4, "character": 33}},
"context": {"diagnostics": []}}}}
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 8, "character": 34}, "end": {"line": 8, "character": 34}},
"context": {"diagnostics": []}}
[{"title": "Import Test1 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 8, "character": 7},
"end": {"line": 8, "character": 34}},
"newText": "Test1"}]}]}},
{"title": "Import test10 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 8, "character": 7},
"end": {"line": 8, "character": 34}},
"newText": "test10"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 17, "character": 34}, "end": {"line": 17, "character": 34}},
"context": {"diagnostics": []}}
[{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 17, "character": 7},
"end": {"line": 17, "character": 34}},
"newText": "Lean.Server.Test.Refs.Test1"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 17, "character": 7},
"end": {"line": 17, "character": 34}},
"newText": "Lean.Server.Test.Refs.test10"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 20, "character": 33}, "end": {"line": 20, "character": 33}},
"context": {"diagnostics": []}}
[{"title": "Import Lean.Server.Test.Refs.test9 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.test9"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test8 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.test8"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test7 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.test7"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test6 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test6"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test5 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test5"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test4 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test4"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test3 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test3"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test2 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test2"}]}]}},
{"title": "Import Lean.Server.Test.Refs.Test1 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.Test1"}]}]}},
{"title": "Import Lean.Server.Test.Refs.test10 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 20, "character": 7},
"end": {"line": 20, "character": 33}},
"newText": "Lean.Server.Test.Refs.test10"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 24, "character": 34}, "end": {"line": 24, "character": 34}},
"context": {"diagnostics": []}}
[{"title": "Import Test1 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 24, "character": 7},
"end": {"line": 24, "character": 34}},
"newText": "Test1"}]}]}},
{"title": "Import test10 from Lean.Server.Test.Refs",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 24, "character": 7},
"end": {"line": 24, "character": 34}},
"newText": "test10"}]}]}},
{"title": "Import all unambiguous unknown identifiers",
"kind": "quickfix",
"data":
{"providerResultIndex": 0,
"providerName": "unknownIdentifiers",
"params":
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 24, "character": 34},
"end": {"line": 24, "character": 34}},
"context": {"diagnostics": []}}}}]
Resolution of Import all unambiguous unknown identifiers:
{"title": "Import all unambiguous unknown identifiers",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 0, "character": 0},
"end": {"line": 0, "character": 0}},
"newText": "import Lean.Server.Test.Refs\n"},
{"range":
{"start": {"line": 13, "character": 7},
"end": {"line": 13, "character": 48}},
"newText": "LeanServerTestRefsTest0'"},
{"range":
{"start": {"line": 24, "character": 7},
"end": {"line": 24, "character": 34}},
"newText": "Test1"},
{"range":
{"start": {"line": 4, "character": 10},
"end": {"line": 4, "character": 33}},
"newText": "LeanServerTestRefsTest0"}]}]},
"data":
{"providerResultIndex": 0,
"providerName": "unknownIdentifiers",
"params":
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 24, "character": 34},
"end": {"line": 24, "character": 34}},
"context": {"diagnostics": []}}}}
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 42, "character": 40}, "end": {"line": 42, "character": 40}},
"context": {"diagnostics": []}}
[{"title": "Change to veryLongAndHopefullyVeryUniqueFoo0",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 42, "character": 7},
"end": {"line": 42, "character": 40}},
"newText": "veryLongAndHopefullyVeryUniqueFoo0"}]}]}},
{"title": "Change to veryLongAndHopefullyVeryUniqueFoobar0",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 42, "character": 7},
"end": {"line": 42, "character": 40}},
"newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 45, "character": 65}, "end": {"line": 45, "character": 65}},
"context": {"diagnostics": []}}
[{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueBar0",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 45, "character": 32},
"end": {"line": 45, "character": 65}},
"newText": "veryLongAndHopefullyVeryUniqueBar0"}]}]}}]
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
"range":
{"start": {"line": 48, "character": 57}, "end": {"line": 48, "character": 57}},
"context": {"diagnostics": []}}
[{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueFoobar0",
"kind": "quickfix",
"edit":
{"documentChanges":
[{"textDocument":
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
"edits":
[{"range":
{"start": {"line": 48, "character": 21},
"end": {"line": 48, "character": 57}},
"newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}]
Reference in a new issue View git blame Copy permalink