diff --git a/spec/ft_spec.lua b/spec/ft_spec.lua index 764e0a34..930fdeda 100644 --- a/spec/ft_spec.lua +++ b/spec/ft_spec.lua @@ -12,7 +12,7 @@ describe('ft.detect', function() end it('detects standard library files', function() - vim.cmd.edit { project.child 'Test/JumpToStdlib.lean', bang = true } + helpers.jump_to_core() assert.are.equal('lean', vim.bo.filetype) local initial_path = vim.api.nvim_buf_get_name(0) diff --git a/spec/helpers.lua b/spec/helpers.lua index c263ac35..8b934bb7 100644 --- a/spec/helpers.lua +++ b/spec/helpers.lua @@ -57,6 +57,19 @@ function helpers.move_cursor(opts) vim.cmd.doautocmd 'CursorMoved' end +--- Jump to an arbitrary file in Lean core. +function helpers.jump_to_core() + vim.cmd.edit(fixtures.project.child 'Test/JumpToStdlib.lean') + vim.cmd.normal '$' + + helpers.wait_for_ready_lsp() + vim.lsp.buf.definition() + + assert.is_truthy(vim.wait(15000, function() + return vim.api.nvim_buf_get_name(0):match '.*/src/lean/.*' + end)) +end + ---@class MoveCursorOpts ---@field window? integer @the window handle. Defaults to the current window. ---@field to table @the new cursor position (1-row indexed, as per nvim_win_set_cursor) diff --git a/spec/helpers_spec.lua b/spec/helpers_spec.lua index 633acd2d..555d7d1a 100644 --- a/spec/helpers_spec.lua +++ b/spec/helpers_spec.lua @@ -84,3 +84,12 @@ describe( end ) ) + +describe('jump_to_core', function() + it('jumps to a file in core Lean', function() + helpers.jump_to_core() + local name = vim.api.nvim_buf_get_name(0) + local is_core = name:match '.*/src/lean/.*' + assert.message("Didn't jump to core Lean!").is_truthy(is_core) + end) +end)