Skip to content

Commit 6215ae0

Browse files
committed
Move a bunch of tests to helpers.search.
1 parent d679279 commit 6215ae0

File tree

6 files changed

+18
-18
lines changed

6 files changed

+18
-18
lines changed

spec/commands_spec.lua

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ describe('LeanGoal', function()
88
it(
99
'shows a popup with the goal',
1010
helpers.clean_buffer('example : 2 = 2 := by sorry', function()
11-
helpers.move_cursor { to = { 1, 20 } }
11+
helpers.search 'sorry'
1212
helpers.wait_for_processing()
1313

1414
local initial_window = Window:current()
@@ -28,7 +28,7 @@ describe('LeanTermGoal', function()
2828
it(
2929
'shows a popup with the term goal',
3030
helpers.clean_buffer('def n : Nat := 37', function()
31-
helpers.move_cursor { to = { 1, 16 } }
31+
helpers.search '37'
3232
helpers.wait_for_processing()
3333

3434
local initial_window = Window:current()

spec/filter_hypothesis_custom_spec.lua

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,13 +16,13 @@ describe(
1616
'filter_hypothesis',
1717
helpers.clean_buffer(
1818
[[
19-
example {A : Type} (n : Nat) (b : 3 = 3) (c : 4 = 4) : n = n ∨ n = 37 := by
20-
left
21-
sorry
22-
]],
19+
example {A : Type} (n : Nat) (b : 3 = 3) (c : 4 = 4) : n = n ∨ n = 37 := by
20+
left
21+
sorry
22+
]],
2323
function()
2424
it('filters hypotheses', function()
25-
helpers.move_cursor { to = { 2, 4 } }
25+
helpers.search 'eft'
2626

2727
assert.infoview_contents.are [[
2828
case h

spec/infoview/autoopen_false_spec.lua

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ describe('infoview', function()
3030

3131
it('allows infoviews to be manually opened', function()
3232
assert.windows.are { lean_window }
33-
helpers.move_cursor { to = { 3, 27 } }
33+
helpers.search 'square 4'
3434
infoview.open()
3535
assert.windows.are { lean_window, infoview.get_current_infoview().window }
3636
assert.infoview_contents.are [[

spec/infoview/plain_contents_spec.lua

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ describe('plain infoviews', function()
1313
it(
1414
'shows goals accomplished on the first line of a solved goal',
1515
helpers.clean_buffer([[example : 37 = 37 := by rfl]], function()
16-
helpers.move_cursor { to = { 1, 26 } }
16+
helpers.search 'rfl'
1717
assert.infoview_contents.are 'Goals accomplished 🎉'
1818
end)
1919
)
@@ -28,7 +28,7 @@ describe('plain infoviews', function()
2828
· sorry
2929
]],
3030
function()
31-
helpers.move_cursor { to = { 2, 3 } }
31+
helpers.search 'ases n'
3232
assert.infoview_contents.are [[
3333
▼ 2 goals
3434
case zero
@@ -367,7 +367,7 @@ describe('plain infoviews', function()
367367
#knownWidget
368368
]],
369369
function()
370-
helpers.move_cursor { to = { 20, 2 } }
370+
helpers.search '^#knownWidget'
371371
assert.infoview_contents.are [[
372372
▼ 20:1-20:13: information:
373373
This will be in the hover.
@@ -395,7 +395,7 @@ describe('plain infoviews', function()
395395
#unknownWidget
396396
]],
397397
function()
398-
helpers.move_cursor { to = { 13, 2 } }
398+
helpers.search '^#unknownWidget'
399399
assert.infoview_contents.are [[
400400
▼ 13:1-13:15: information:
401401
You're gonna see this alternate text.

spec/widgets/core_spec.lua

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ describe('Lean core widgets', function()
3333
apply?
3434
]],
3535
function()
36-
helpers.move_cursor { to = { 2, 2 } }
36+
helpers.search 'apply'
3737
assert.infoview_contents.are [[
3838
Goals accomplished 🎉
3939
@@ -65,7 +65,7 @@ describe('Lean core widgets', function()
6565
example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact?
6666
]],
6767
function()
68-
helpers.move_cursor { to = { 1, 100 } }
68+
helpers.search 'xact'
6969
assert.infoview_contents.are [[
7070
Goals accomplished 🎉
7171
@@ -103,7 +103,7 @@ describe('Lean core widgets', function()
103103
foo
104104
]],
105105
function()
106-
helpers.move_cursor { to = { 11, 2 } }
106+
helpers.search [[ \zsfoo]]
107107
assert.infoview_contents.are [[
108108
⊢ True
109109
@@ -134,7 +134,7 @@ describe('Lean core widgets', function()
134134
end Lean.Meta.Tactic.TryThis
135135
]],
136136
function()
137-
helpers.move_cursor { to = { 10, 28 } }
137+
helpers.search [[by \zstwoSuggestions]]
138138
assert.infoview_contents.are [[
139139
⊢ 37 = 37
140140

spec/widgets/importgraph_spec.lua

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,14 @@ describe('ImportGraph widgets', function()
2121
function()
2222
local initial = Buffer:current()
2323

24-
helpers.move_cursor { to = { 2, 2 } }
24+
helpers.search 'find_home'
2525
assert.infoview_contents.are [[
2626
▼ 2:1-2:11: information:
2727
[Init.Prelude]
2828
]]
2929

3030
infoview.go_to()
31-
helpers.move_cursor { to = { 2, 2 } }
31+
helpers.search 'Init'
3232
helpers.feed 'gd'
3333

3434
assert.is_truthy(vim.wait(15000, function()

0 commit comments

Comments
 (0)