feat: jumpToEnd

README.md

@@ -39,6 +39,8 @@ lua require'vscoq'.setup()
         * `:VsCoq check {pattern}`
         * `:VsCoq print {pattern}`
         * `:VsCoq locate {pattern}`
+    * etc
+        * `:VsCoq jumpToEnd`: Jump to the end of the checked region.
 * [Commands from nvim-lspconfig](https://github.com/neovim/nvim-lspconfig#commands)
   work as expected.
   For example, run `:LspRestart` to restart `vscoqtop`.

lua/vscoq/client.lua

@@ -11,7 +11,7 @@ local render = require('vscoq.render')
 -- for now we have a single proofview panel.
 -- Once fixed, make config for single/multi proofview.
 -- ---@field buffers table<buffer, { proofview_bufnr: buffer }>
----@field buffers table<buffer, true>
+---@field buffers table<buffer, { highlights: vscoq.UpdateHighlightsNotification }>
 ---@field proofview_panel buffer
 ---@field query_panel buffer
 ---@field query_id integer latest query id. Only the latest query result is displayed.
@@ -66,6 +66,7 @@ commands[#commands + 1] = 'continuous'
 function VSCoqNvim:updateHighlights(highlights)
   local bufnr = vim.uri_to_bufnr(highlights.uri)
   vim.api.nvim_buf_clear_namespace(bufnr, self.highlight_ns, 0, -1)
+  self.buffers[bufnr].highlights = highlights
   -- for _, range in ipairs(highlights.processingRange) do
   for _, range in ipairs(highlights.processedRange) do
     vim.highlight.range(
@@ -79,6 +80,27 @@ function VSCoqNvim:updateHighlights(highlights)
   end
 end
 
+function VSCoqNvim:jumpToEnd()
+  local win = vim.api.nvim_get_current_win()
+  local bufnr = vim.api.nvim_win_get_buf(win)
+  if not self.buffers[bufnr] then
+    return
+  end
+
+  local max_end
+  for _, range in ipairs(self.buffers[bufnr].highlights.processedRange) do
+    local end_ = util.position_lsp_to_api(bufnr, range['end'], self.lc.offset_encoding)
+    if max_end == nil or util.api_position_lt(max_end, end_) then
+      max_end = end_
+    end
+  end
+  if max_end then
+    vim.api.nvim_win_set_cursor(win, util.position_api_to_mark(max_end))
+  end
+end
+
+commands[#commands + 1] = 'jumpToEnd'
+
 ---@param target vscoq.MoveCursorNotification
 function VSCoqNvim:moveCursor(target)
   local bufnr = vim.uri_to_bufnr(target.uri)
@@ -345,7 +367,7 @@ end
 ---@param bufnr buffer
 function VSCoqNvim:attach(bufnr)
   assert(self.buffers[bufnr] == nil)
-  self.buffers[bufnr] = true
+  self.buffers[bufnr] = {}
 
   vim.api.nvim_create_autocmd({ 'CursorMoved', 'CursorMovedI' }, {
     group = self.ag,

lua/vscoq/util.lua

@@ -20,6 +20,19 @@ function M.position_api_to_mark(position)
   return { position[1] + 1, position[2] }
 end
 
+---@param p1 APIPosition
+---@param p2 APIPosition
+---@return boolean
+function M.api_position_lt(p1, p2)
+  if p1[1] < p2[1] then
+    return true
+  elseif p1[1] == p2[1] then
+    return p1[2] < p2[2]
+  else
+    return false
+  end
+end
+
 ---@param bufnr buffer
 ---@param position MarkPosition
 ---@param offset_encoding lsp.PositionEncodingKind
@@ -62,7 +75,7 @@ end
 ---@param bufnr integer
 ---@param method string
 ---@param params table
----@param handler? lsp-handler
+---@param handler? lsp.Handler
 ---@return fun()|nil cancel function to cancel the request
 function M.request_async(client, bufnr, method, params, handler)
   local request_success, request_id = client.request(method, params, handler, bufnr)