diff --git a/src/Lean/Server/Completion/CompletionUtils.lean b/src/Lean/Server/Completion/CompletionUtils.lean index 32bdaa98b7..94e098091a 100644 --- a/src/Lean/Server/Completion/CompletionUtils.lean +++ b/src/Lean/Server/Completion/CompletionUtils.lean @@ -41,13 +41,13 @@ structure ContextualizedCompletionInfo where ctx : ContextInfo info : CompletionInfo -def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name) +partial def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List OpenDecl) (id : Name) : Name := Id.run do - let mut minimized := shortenIn id currNamespace + let mut minimized := shortenInCurrentNamespace id currNamespace for openDecl in openDecls do let candidate? := match openDecl with | .simple ns except => - let candidate := shortenIn id ns + let candidate := shortenInOpenNamespace id ns if ! except.contains candidate then some candidate else @@ -62,13 +62,20 @@ def minimizeGlobalIdentifierInContext (currNamespace : Name) (openDecls : List O minimized := candidate return minimized where - shortenIn (id : Name) (contextNamespace : Name) : Name := - if contextNamespace matches .anonymous then + shortenInCurrentNamespace (id : Name) (currentNamespace : Name) : Name := + if currentNamespace matches .anonymous then id - else if contextNamespace.isPrefixOf id then - id.replacePrefix contextNamespace .anonymous else + let maybeShortened := shortenInOpenNamespace id currentNamespace + if maybeShortened != id then + maybeShortened + else + shortenInCurrentNamespace id currentNamespace.getPrefix + shortenInOpenNamespace (id : Name) (openNamespace : Name) : Name := + if openNamespace == id then id + else + id.replacePrefix openNamespace .anonymous def unfoldDefinitionGuarded? (e : Expr) : MetaM (Option Expr) := try Lean.Meta.unfoldDefinition? e catch _ => pure none diff --git a/src/Lean/Server/Test/Refs.lean b/src/Lean/Server/Test/Refs.lean index a44230a1cc..2550dbf3a5 100644 --- a/src/Lean/Server/Test/Refs.lean +++ b/src/Lean/Server/Test/Refs.lean @@ -11,6 +11,8 @@ import Init.Prelude public def LeanServerTestRefsTest0 := Nat +public def Lean.Server.Test.LeanServerTestRefsTest0' := Nat + namespace Lean.Server.Test.Refs public def Test1 := Nat diff --git a/tests/lean/interactive/findReferences.lean.expected.out b/tests/lean/interactive/findReferences.lean.expected.out index ae4e80c992..3194ac4199 100644 --- a/tests/lean/interactive/findReferences.lean.expected.out +++ b/tests/lean/interactive/findReferences.lean.expected.out @@ -18,13 +18,13 @@ {"start": {"line": 9, "character": 13}, "end": {"line": 9, "character": 40}}}, {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 15, "character": 11}, - "end": {"line": 15, "character": 16}}}, + {"start": {"line": 17, "character": 11}, + "end": {"line": 17, "character": 16}}}, {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 16, "character": 20}, - "end": {"line": 16, "character": 25}}}, + {"start": {"line": 18, "character": 20}, + "end": {"line": 18, "character": 25}}}, {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 17, "character": 20}, - "end": {"line": 17, "character": 25}}}] + {"start": {"line": 19, "character": 20}, + "end": {"line": 19, "character": 25}}}] diff --git a/tests/lean/interactive/incomingCallHierarchy.lean.expected.out b/tests/lean/interactive/incomingCallHierarchy.lean.expected.out index 71834e8214..6ae5bd0a84 100644 --- a/tests/lean/interactive/incomingCallHierarchy.lean.expected.out +++ b/tests/lean/interactive/incomingCallHierarchy.lean.expected.out @@ -45,11 +45,11 @@ [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 15, "character": 11}, - "end": {"line": 15, "character": 16}}, + {"start": {"line": 17, "character": 11}, + "end": {"line": 17, "character": 16}}, "range": - {"start": {"line": 15, "character": 11}, - "end": {"line": 15, "character": 16}}, + {"start": {"line": 17, "character": 11}, + "end": {"line": 17, "character": 16}}, "name": "Lean.Server.Test.Refs.Test1", "kind": 14, "data": @@ -59,70 +59,70 @@ [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 16, "character": 11}, - "end": {"line": 16, "character": 16}}, + {"start": {"line": 18, "character": 11}, + "end": {"line": 18, "character": 16}}, "range": - {"start": {"line": 16, "character": 0}, - "end": {"line": 16, "character": 25}}, + {"start": {"line": 18, "character": 0}, + "end": {"line": 18, "character": 25}}, "name": "Lean.Server.Test.Refs.Test2", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test2", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 16, "character": 20}, - "end": {"line": 16, "character": 25}}], + [{"start": {"line": 18, "character": 20}, + "end": {"line": 18, "character": 25}}], "children": [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 18, "character": 11}, - "end": {"line": 18, "character": 16}}, + {"start": {"line": 20, "character": 11}, + "end": {"line": 20, "character": 16}}, "range": - {"start": {"line": 18, "character": 0}, - "end": {"line": 18, "character": 25}}, + {"start": {"line": 20, "character": 0}, + "end": {"line": 20, "character": 25}}, "name": "Lean.Server.Test.Refs.Test4", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test4", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 18, "character": 20}, - "end": {"line": 18, "character": 25}}], + [{"start": {"line": 20, "character": 20}, + "end": {"line": 20, "character": 25}}], "children": []}, {"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 19, "character": 11}, - "end": {"line": 19, "character": 16}}, + {"start": {"line": 21, "character": 11}, + "end": {"line": 21, "character": 16}}, "range": - {"start": {"line": 19, "character": 0}, - "end": {"line": 19, "character": 25}}, + {"start": {"line": 21, "character": 0}, + "end": {"line": 21, "character": 25}}, "name": "Lean.Server.Test.Refs.Test5", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test5", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 19, "character": 20}, - "end": {"line": 19, "character": 25}}], + [{"start": {"line": 21, "character": 20}, + "end": {"line": 21, "character": 25}}], "children": []}]}, {"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 17, "character": 11}, - "end": {"line": 17, "character": 16}}, + {"start": {"line": 19, "character": 11}, + "end": {"line": 19, "character": 16}}, "range": - {"start": {"line": 17, "character": 0}, - "end": {"line": 17, "character": 25}}, + {"start": {"line": 19, "character": 0}, + "end": {"line": 19, "character": 25}}, "name": "Lean.Server.Test.Refs.Test3", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test3", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 17, "character": 20}, - "end": {"line": 17, "character": 25}}], + [{"start": {"line": 19, "character": 20}, + "end": {"line": 19, "character": 25}}], "children": []}, {"item": {"uri": "file:///incomingCallHierarchy.lean", diff --git a/tests/lean/interactive/outgoingCallHierarchy.lean.expected.out b/tests/lean/interactive/outgoingCallHierarchy.lean.expected.out index 9e030b5e12..3d47c80f7c 100644 --- a/tests/lean/interactive/outgoingCallHierarchy.lean.expected.out +++ b/tests/lean/interactive/outgoingCallHierarchy.lean.expected.out @@ -286,11 +286,11 @@ [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 26, "character": 11}, - "end": {"line": 26, "character": 17}}, + {"start": {"line": 28, "character": 11}, + "end": {"line": 28, "character": 17}}, "range": - {"start": {"line": 26, "character": 11}, - "end": {"line": 26, "character": 17}}, + {"start": {"line": 28, "character": 11}, + "end": {"line": 28, "character": 17}}, "name": "Lean.Server.Test.Refs.test10", "kind": 14, "data": @@ -303,70 +303,70 @@ [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 25, "character": 11}, - "end": {"line": 25, "character": 16}}, + {"start": {"line": 27, "character": 11}, + "end": {"line": 27, "character": 16}}, "range": - {"start": {"line": 25, "character": 11}, - "end": {"line": 25, "character": 16}}, + {"start": {"line": 27, "character": 11}, + "end": {"line": 27, "character": 16}}, "name": "Lean.Server.Test.Refs.test9", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.test9", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 26, "character": 21}, - "end": {"line": 26, "character": 26}}], + [{"start": {"line": 28, "character": 21}, + "end": {"line": 28, "character": 26}}], "children": [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 23, "character": 11}, - "end": {"line": 23, "character": 16}}, + {"start": {"line": 25, "character": 11}, + "end": {"line": 25, "character": 16}}, "range": - {"start": {"line": 23, "character": 11}, - "end": {"line": 23, "character": 16}}, + {"start": {"line": 25, "character": 11}, + "end": {"line": 25, "character": 16}}, "name": "Lean.Server.Test.Refs.test7", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.test7", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 25, "character": 20}, - "end": {"line": 25, "character": 25}}], + [{"start": {"line": 27, "character": 20}, + "end": {"line": 27, "character": 25}}], "children": [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 21, "character": 17}, - "end": {"line": 21, "character": 22}}, + {"start": {"line": 23, "character": 17}, + "end": {"line": 23, "character": 22}}, "range": - {"start": {"line": 21, "character": 17}, - "end": {"line": 21, "character": 22}}, + {"start": {"line": 23, "character": 17}, + "end": {"line": 23, "character": 22}}, "name": "Lean.Server.Test.Refs.Test6", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test6", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 23, "character": 19}, - "end": {"line": 23, "character": 24}}], + [{"start": {"line": 25, "character": 19}, + "end": {"line": 25, "character": 24}}], "children": []}, {"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 22, "character": 4}, - "end": {"line": 22, "character": 6}}, + {"start": {"line": 24, "character": 4}, + "end": {"line": 24, "character": 6}}, "range": - {"start": {"line": 22, "character": 4}, - "end": {"line": 22, "character": 6}}, + {"start": {"line": 24, "character": 4}, + "end": {"line": 24, "character": 6}}, "name": "Lean.Server.Test.Refs.Test6.mk", "kind": 14, "data": {"name": "Lean.Server.Test.Refs.Test6.mk", "module": "Lean.Server.Test.Refs"}}, "fromRanges": - [{"start": {"line": 23, "character": 28}, - "end": {"line": 23, "character": 31}}], + [{"start": {"line": 25, "character": 28}, + "end": {"line": 25, "character": 31}}], "children": []}]}]}]}, {"item": {"uri": "file:///outgoingCallHierarchy.lean", @@ -694,11 +694,11 @@ [{"item": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "selectionRange": - {"start": {"line": 21, "character": 17}, - "end": {"line": 21, "character": 22}}, + {"start": {"line": 23, "character": 17}, + "end": {"line": 23, "character": 22}}, "range": - {"start": {"line": 21, "character": 17}, - "end": {"line": 21, "character": 22}}, + {"start": {"line": 23, "character": 17}, + "end": {"line": 23, "character": 22}}, "name": "Lean.Server.Test.Refs.Test6", "kind": 14, "data": diff --git a/tests/lean/interactive/unknownIdentifierCodeActions.lean b/tests/lean/interactive/unknownIdentifierCodeActions.lean index 6e8a8dc93f..d2c8f58c80 100644 --- a/tests/lean/interactive/unknownIdentifierCodeActions.lean +++ b/tests/lean/interactive/unknownIdentifierCodeActions.lean @@ -5,9 +5,28 @@ example : LeanServerTestRefsTest0 --^ codeAction +namespace Lean.Server.Test.Refs +#check Lean.Server.Test.Refs.test1 + --^ codeAction +end Lean.Server.Test.Refs + +namespace Lean.Server.Test.Refs.Foobar +#check Lean.Server.Test.LeanServerTestRefsTest0' +end Lean.Server.Test.Refs.Foobar + +open Lean.Server.Test.Refs.Foobar +#check Lean.Server.Test.Refs.test1 + --^ codeAction + #check Lean.Server.Test.Refs.test --^ codeAction +namespace Lean.Server.Test.Refs.Test1 +#check Lean.Server.Test.Refs.Test1 + --^ codeAction +end Lean.Server.Test.Refs.Test1 + + structure Foobar where veryLongAndHopefullyVeryUniqueBar0 : Nat diff --git a/tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out b/tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out index 8c4f289c1e..82bb04492c 100644 --- a/tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out +++ b/tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out @@ -51,6 +51,22 @@ {"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": @@ -89,6 +105,14 @@ Resolution of Import all unambiguous unknown identifiers: {"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}}, @@ -103,9 +127,9 @@ Resolution of Import all unambiguous unknown identifiers: "context": {"diagnostics": []}}}} {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"}, "range": - {"start": {"line": 7, "character": 33}, "end": {"line": 7, "character": 33}}, + {"start": {"line": 8, "character": 34}, "end": {"line": 8, "character": 34}}, "context": {"diagnostics": []}} -[{"title": "Import Lean.Server.Test.Refs.test9 from Lean.Server.Test.Refs", +[{"title": "Import Test1 from Lean.Server.Test.Refs", "kind": "quickfix", "edit": {"documentChanges": @@ -117,10 +141,10 @@ Resolution of Import all unambiguous unknown identifiers: "end": {"line": 0, "character": 0}}, "newText": "import Lean.Server.Test.Refs\n"}, {"range": - {"start": {"line": 7, "character": 7}, - "end": {"line": 7, "character": 33}}, - "newText": "Lean.Server.Test.Refs.test9"}]}]}}, - {"title": "Import Lean.Server.Test.Refs.test8 from Lean.Server.Test.Refs", + {"start": {"line": 8, "character": 7}, + "end": {"line": 8, "character": 34}}, + "newText": "Test1"}]}]}}, + {"title": "Import test10 from Lean.Server.Test.Refs", "kind": "quickfix", "edit": {"documentChanges": @@ -132,10 +156,14 @@ Resolution of Import all unambiguous unknown identifiers: "end": {"line": 0, "character": 0}}, "newText": "import Lean.Server.Test.Refs\n"}, {"range": - {"start": {"line": 7, "character": 7}, - "end": {"line": 7, "character": 33}}, - "newText": "Lean.Server.Test.Refs.test8"}]}]}}, - {"title": "Import Lean.Server.Test.Refs.test7 from Lean.Server.Test.Refs", + {"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": @@ -147,98 +175,8 @@ Resolution of Import all unambiguous unknown identifiers: "end": {"line": 0, "character": 0}}, "newText": "import Lean.Server.Test.Refs\n"}, {"range": - {"start": {"line": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "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": 7, "character": 7}, - "end": {"line": 7, "character": 33}}, + {"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", @@ -252,12 +190,244 @@ Resolution of Import all unambiguous unknown identifiers: "end": {"line": 0, "character": 0}}, "newText": "import Lean.Server.Test.Refs\n"}, {"range": - {"start": {"line": 7, "character": 7}, - "end": {"line": 7, "character": 33}}, + {"start": {"line": 17, "character": 7}, + "end": {"line": 17, "character": 34}}, "newText": "Lean.Server.Test.Refs.test10"}]}]}}] {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"}, "range": - {"start": {"line": 23, "character": 40}, "end": {"line": 23, "character": 40}}, + {"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", @@ -267,8 +437,8 @@ Resolution of Import all unambiguous unknown identifiers: {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"}, "edits": [{"range": - {"start": {"line": 23, "character": 7}, - "end": {"line": 23, "character": 40}}, + {"start": {"line": 42, "character": 7}, + "end": {"line": 42, "character": 40}}, "newText": "veryLongAndHopefullyVeryUniqueFoo0"}]}]}}, {"title": "Change to veryLongAndHopefullyVeryUniqueFoobar0", "kind": "quickfix", @@ -278,12 +448,12 @@ Resolution of Import all unambiguous unknown identifiers: {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"}, "edits": [{"range": - {"start": {"line": 23, "character": 7}, - "end": {"line": 23, "character": 40}}, + {"start": {"line": 42, "character": 7}, + "end": {"line": 42, "character": 40}}, "newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}] {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"}, "range": - {"start": {"line": 26, "character": 65}, "end": {"line": 26, "character": 65}}, + {"start": {"line": 45, "character": 65}, "end": {"line": 45, "character": 65}}, "context": {"diagnostics": []}} [{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueBar0", "kind": "quickfix", @@ -293,12 +463,12 @@ Resolution of Import all unambiguous unknown identifiers: {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"}, "edits": [{"range": - {"start": {"line": 26, "character": 32}, - "end": {"line": 26, "character": 65}}, + {"start": {"line": 45, "character": 32}, + "end": {"line": 45, "character": 65}}, "newText": "veryLongAndHopefullyVeryUniqueBar0"}]}]}}] {"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"}, "range": - {"start": {"line": 29, "character": 57}, "end": {"line": 29, "character": 57}}, + {"start": {"line": 48, "character": 57}, "end": {"line": 48, "character": 57}}, "context": {"diagnostics": []}} [{"title": "Change to Foobar.veryLongAndHopefullyVeryUniqueFoobar0", "kind": "quickfix", @@ -308,6 +478,6 @@ Resolution of Import all unambiguous unknown identifiers: {"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"}, "edits": [{"range": - {"start": {"line": 29, "character": 21}, - "end": {"line": 29, "character": 57}}, + {"start": {"line": 48, "character": 21}, + "end": {"line": 48, "character": 57}}, "newText": "veryLongAndHopefullyVeryUniqueFoobar0"}]}]}}] diff --git a/tests/lean/interactive/workspaceSymbols.lean.expected.out b/tests/lean/interactive/workspaceSymbols.lean.expected.out index 156cccd074..a08ba74476 100644 --- a/tests/lean/interactive/workspaceSymbols.lean.expected.out +++ b/tests/lean/interactive/workspaceSymbols.lean.expected.out @@ -12,43 +12,59 @@ "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 25, "character": 11}, - "end": {"line": 25, "character": 16}}}, + {"start": {"line": 27, "character": 11}, + "end": {"line": 27, "character": 16}}}, "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.test8", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 24, "character": 11}, - "end": {"line": 24, "character": 16}}}, + {"start": {"line": 26, "character": 11}, + "end": {"line": 26, "character": 16}}}, "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.test7", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 23, "character": 11}, - "end": {"line": 23, "character": 16}}}, + {"start": {"line": 25, "character": 11}, + "end": {"line": 25, "character": 16}}}, "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.Test6", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 21, "character": 17}, - "end": {"line": 21, "character": 22}}}, + {"start": {"line": 23, "character": 17}, + "end": {"line": 23, "character": 22}}}, "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.Test5", "location": + {"uri": "file:///src/Lean/Server/Test/Refs.lean", + "range": + {"start": {"line": 21, "character": 11}, + "end": {"line": 21, "character": 16}}}, + "kind": 14}, + {"tags": [], + "name": "Lean.Server.Test.Refs.Test4", + "location": + {"uri": "file:///src/Lean/Server/Test/Refs.lean", + "range": + {"start": {"line": 20, "character": 11}, + "end": {"line": 20, "character": 16}}}, + "kind": 14}, + {"tags": [], + "name": "Lean.Server.Test.Refs.Test3", + "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": {"start": {"line": 19, "character": 11}, "end": {"line": 19, "character": 16}}}, "kind": 14}, {"tags": [], - "name": "Lean.Server.Test.Refs.Test4", + "name": "Lean.Server.Test.Refs.Test2", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": @@ -56,42 +72,26 @@ "end": {"line": 18, "character": 16}}}, "kind": 14}, {"tags": [], - "name": "Lean.Server.Test.Refs.Test3", + "name": "Lean.Server.Test.Refs.Test1", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": {"start": {"line": 17, "character": 11}, "end": {"line": 17, "character": 16}}}, "kind": 14}, - {"tags": [], - "name": "Lean.Server.Test.Refs.Test2", - "location": - {"uri": "file:///src/Lean/Server/Test/Refs.lean", - "range": - {"start": {"line": 16, "character": 11}, - "end": {"line": 16, "character": 16}}}, - "kind": 14}, - {"tags": [], - "name": "Lean.Server.Test.Refs.Test1", - "location": - {"uri": "file:///src/Lean/Server/Test/Refs.lean", - "range": - {"start": {"line": 15, "character": 11}, - "end": {"line": 15, "character": 16}}}, - "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.test10", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 26, "character": 11}, - "end": {"line": 26, "character": 17}}}, + {"start": {"line": 28, "character": 11}, + "end": {"line": 28, "character": 17}}}, "kind": 14}, {"tags": [], "name": "Lean.Server.Test.Refs.Test6.mk", "location": {"uri": "file:///src/Lean/Server/Test/Refs.lean", "range": - {"start": {"line": 22, "character": 4}, - "end": {"line": 22, "character": 6}}}, + {"start": {"line": 24, "character": 4}, + "end": {"line": 24, "character": 6}}}, "kind": 14}]