Skip to content

Commit db0bee7

Browse files
KhaKha
committed
revert test change
1 parent 3ae3241 commit db0bee7

File tree

2 files changed

+2
-89
lines changed

2 files changed

+2
-89
lines changed

‎tests/lean/interactive/unknownIdentifierCodeActions.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ module
33

44
public section
55

6-
#check Lean.Server.Test.Refs.Test1
6+
#check Lean.Server.Test.Refs.test1
77
--^ codeAction
88

99
example : LeanServerTestRefsTest0

‎tests/lean/interactive/unknownIdentifierCodeActions.lean.expected.out‎

Lines changed: 1 addition & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -31,70 +31,7 @@
3131
{"range":
3232
{"start": {"line": 5, "character": 7},
3333
"end": {"line": 5, "character": 34}},
34-
"newText": "Lean.Server.Test.Refs.test10"}]}]}},
35-
{"title": "Import all unambiguous unknown identifiers",
36-
"kind": "quickfix",
37-
"data":
38-
{"providerResultIndex": 0,
39-
"providerName": "unknownIdentifiers",
40-
"params":
41-
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
42-
"range":
43-
{"start": {"line": 5, "character": 34},
44-
"end": {"line": 5, "character": 34}},
45-
"context": {"diagnostics": []}}}}]
46-
Resolution of Import all unambiguous unknown identifiers:
47-
{"title": "Import all unambiguous unknown identifiers",
48-
"kind": "quickfix",
49-
"edit":
50-
{"documentChanges":
51-
[{"textDocument":
52-
{"version": 1, "uri": "file:///unknownIdentifierCodeActions.lean"},
53-
"edits":
54-
[{"range":
55-
{"start": {"line": 1, "character": 0},
56-
"end": {"line": 1, "character": 0}},
57-
"newText": "import Lean.Server.Test.Refs\n"},
58-
{"range":
59-
{"start": {"line": 5, "character": 7},
60-
"end": {"line": 5, "character": 34}},
61-
"newText": "Lean.Server.Test.Refs.Test1"},
62-
{"range":
63-
{"start": {"line": 17, "character": 7},
64-
"end": {"line": 17, "character": 48}},
65-
"newText": "LeanServerTestRefsTest0'"},
66-
{"range":
67-
{"start": {"line": 28, "character": 7},
68-
"end": {"line": 28, "character": 34}},
69-
"newText": "Test1"},
70-
{"range":
71-
{"start": {"line": 55, "character": 20},
72-
"end": {"line": 55, "character": 47}},
73-
"newText": "Lean.Server.Test.Refs.Test1"},
74-
{"range":
75-
{"start": {"line": 57, "character": 5},
76-
"end": {"line": 57, "character": 32}},
77-
"newText": "Lean.Server.Test.Refs.Test1"},
78-
{"range":
79-
{"start": {"line": 60, "character": 26},
80-
"end": {"line": 60, "character": 53}},
81-
"newText": "Lean.Server.Test.Refs.Test1"},
82-
{"range":
83-
{"start": {"line": 62, "character": 5},
84-
"end": {"line": 62, "character": 32}},
85-
"newText": "Lean.Server.Test.Refs.Test1"},
86-
{"range":
87-
{"start": {"line": 8, "character": 10},
88-
"end": {"line": 8, "character": 33}},
89-
"newText": "LeanServerTestRefsTest0"}]}]},
90-
"data":
91-
{"providerResultIndex": 0,
92-
"providerName": "unknownIdentifiers",
93-
"params":
94-
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
95-
"range":
96-
{"start": {"line": 5, "character": 34}, "end": {"line": 5, "character": 34}},
97-
"context": {"diagnostics": []}}}}
34+
"newText": "Lean.Server.Test.Refs.test10"}]}]}}]
9835
{"textDocument": {"uri": "file:///unknownIdentifierCodeActions.lean"},
9936
"range":
10037
{"start": {"line": 8, "character": 33}, "end": {"line": 8, "character": 33}},
@@ -168,10 +105,6 @@ Resolution of Import all unambiguous unknown identifiers:
168105
{"start": {"line": 1, "character": 0},
169106
"end": {"line": 1, "character": 0}},
170107
"newText": "import Lean.Server.Test.Refs\n"},
171-
{"range":
172-
{"start": {"line": 5, "character": 7},
173-
"end": {"line": 5, "character": 34}},
174-
"newText": "Lean.Server.Test.Refs.Test1"},
175108
{"range":
176109
{"start": {"line": 17, "character": 7},
177110
"end": {"line": 17, "character": 48}},
@@ -487,10 +420,6 @@ Resolution of Import all unambiguous unknown identifiers:
487420
{"start": {"line": 1, "character": 0},
488421
"end": {"line": 1, "character": 0}},
489422
"newText": "import Lean.Server.Test.Refs\n"},
490-
{"range":
491-
{"start": {"line": 5, "character": 7},
492-
"end": {"line": 5, "character": 34}},
493-
"newText": "Lean.Server.Test.Refs.Test1"},
494423
{"range":
495424
{"start": {"line": 17, "character": 7},
496425
"end": {"line": 17, "character": 48}},
@@ -641,10 +570,6 @@ Resolution of Import all unambiguous unknown identifiers:
641570
{"start": {"line": 1, "character": 0},
642571
"end": {"line": 1, "character": 0}},
643572
"newText": "import Lean.Server.Test.Refs\n"},
644-
{"range":
645-
{"start": {"line": 5, "character": 7},
646-
"end": {"line": 5, "character": 34}},
647-
"newText": "Lean.Server.Test.Refs.Test1"},
648573
{"range":
649574
{"start": {"line": 17, "character": 7},
650575
"end": {"line": 17, "character": 48}},
@@ -739,10 +664,6 @@ Resolution of Import all unambiguous unknown identifiers:
739664
{"start": {"line": 1, "character": 0},
740665
"end": {"line": 1, "character": 0}},
741666
"newText": "import Lean.Server.Test.Refs\n"},
742-
{"range":
743-
{"start": {"line": 5, "character": 7},
744-
"end": {"line": 5, "character": 34}},
745-
"newText": "Lean.Server.Test.Refs.Test1"},
746667
{"range":
747668
{"start": {"line": 17, "character": 7},
748669
"end": {"line": 17, "character": 48}},
@@ -837,10 +758,6 @@ Resolution of Import all unambiguous unknown identifiers:
837758
{"start": {"line": 1, "character": 0},
838759
"end": {"line": 1, "character": 0}},
839760
"newText": "import Lean.Server.Test.Refs\n"},
840-
{"range":
841-
{"start": {"line": 5, "character": 7},
842-
"end": {"line": 5, "character": 34}},
843-
"newText": "Lean.Server.Test.Refs.Test1"},
844761
{"range":
845762
{"start": {"line": 17, "character": 7},
846763
"end": {"line": 17, "character": 48}},
@@ -935,10 +852,6 @@ Resolution of Import all unambiguous unknown identifiers:
935852
{"start": {"line": 1, "character": 0},
936853
"end": {"line": 1, "character": 0}},
937854
"newText": "import Lean.Server.Test.Refs\n"},
938-
{"range":
939-
{"start": {"line": 5, "character": 7},
940-
"end": {"line": 5, "character": 34}},
941-
"newText": "Lean.Server.Test.Refs.Test1"},
942855
{"range":
943856
{"start": {"line": 17, "character": 7},
944857
"end": {"line": 17, "character": 48}},

0 commit comments

Comments
 (0)