Fix splitting terms with inner colons in our interactive hovers.

This fixes the example from the issue and is a bit more robust,
though this specific feature may still be more trouble than
it's worth without actually writing the RFC for upstream support.

Closes: #521

Author: Julian

lua/lean/hover.lua

@@ -55,6 +55,25 @@ local function apply_lean_syntax(buffer, last_line)
   end)
 end
 
+---Find the byte index of the top-level `:` in a Lean signature, i.e. the
+---colon that separates the binder list from the result type.  Bracket-aware
+---so colons inside binders such as `(x : T)` or `{x : T}` are skipped.
+---@param signature string
+---@return integer? index 1-based byte index of the `:` character, or nil if none
+local function top_level_colon(signature)
+  local depth = 0
+  for i = 1, #signature do
+    local c = signature:sub(i, i)
+    if c == '(' or c == '{' or c == '[' then
+      depth = depth + 1
+    elseif c == ')' or c == '}' or c == ']' then
+      depth = depth - 1
+    elseif c == ':' and depth == 0 and signature:sub(i + 1, i + 1) ~= '=' then
+      return i
+    end
+  end
+end
+
 ---Extract the signature and documentation from a Lean hover result.
 ---
 ---Lean's hover markdown has the form:
@@ -68,7 +87,7 @@ end
 ---    *import Module*
 ---
 ---We show the type interactively via RPC, so we extract the expression
----name/signature (everything before the final ` : ` in the code fence)
+---name/signature (everything before the top-level `:` in the code fence)
 ---and the documentation (everything after the first `***` separator).
 ---@param result table the LSP hover result
 ---@return string? signature the expression signature (without the type)
@@ -79,12 +98,20 @@ local function extract_hover(result)
     return
   end
 
-  -- Extract the expression name from inside the code fence.
-  -- The fence contains lines like "Nat.add : Nat → Nat → Nat" or
-  -- "foo (n : Nat) : Nat".  The greedy (.+) finds the last " : ",
-  -- which separates the expression from its type.
+  -- Extract the expression name from inside the code fence.  The fence
+  -- contains lines like `Nat.add : Nat → Nat → Nat` or `foo (n : Nat) : Nat`,
+  -- and for multi-line signatures the top-level `:` can be at end of a line
+  -- with no trailing space.  We walk the fence tracking bracket depth so
+  -- colons inside binders never split the signature.
   local fence = value:match '^```lean\n(.-)```'
-  local signature = fence and vim.trim(fence):match '(.+) : '
+  local signature
+  if fence then
+    local trimmed = vim.trim(fence)
+    local colon = top_level_colon(trimmed)
+    if colon then
+      signature = vim.trim(trimmed:sub(1, colon - 1))
+    end
+  end
 
   -- Extract documentation after the first *** separator.  Lean uses `***`
   -- as a thematic break; we convert to `---` for nicer rendering, but pad

spec/hover_spec.lua

@@ -16,6 +16,9 @@ describe(
     [[
       #check Nat
       #check @Nat.add
+      theorem mlt_521_repro {α : Type} {β : Type} (h_a : α = β) (h_b : β = α) (h_c : α = β) (h_d : β = α) :
+          (∀ x : α, x = x) ∧ (∀ y : β, y = y) ∧ (∀ z : α, z = z) ∧ (∀ w : β, w = w) :=
+        sorry
     ]],
     function()
       local lean_window = Window:current()
@@ -148,6 +151,48 @@ describe(
         lean_window:make_current()
       end)
 
+      it('preserves multi-line signatures whose binders contain colons', function()
+        lean_window:make_current()
+        -- Hover on the theorem name in its declaration on line 3.
+        helpers.move_cursor { to = { 3, 10 } }
+
+        local ids = { lean_window.id, current_infoview.window.id }
+
+        hover()
+        -- Poll until the hover window actually contains our theorem signature;
+        -- the interactive-hover RPC can take longer than the default 1s
+        -- `wait_for_new_window` allows.
+        local hover_win
+        local ok = vim.wait(15000, function()
+          hover_win = vim.iter(vim.api.nvim_tabpage_list_wins(0)):find(function(w)
+            if vim.tbl_contains(ids, w) then
+              return false
+            end
+            local buf = vim.api.nvim_win_get_buf(w)
+            local lines = vim.api.nvim_buf_get_lines(buf, 0, -1, false)
+            return table.concat(lines, '\n'):match 'mlt_521_repro' ~= nil
+          end)
+          return hover_win ~= nil
+        end)
+        assert.message('Interactive hover never rendered.').is_true(ok)
+        hover_win = Window:from_id(hover_win)
+
+        local contents = table.concat(hover_win:buffer():lines(), '\n')
+
+        -- Regression for #521: the parser used to split the signature at a
+        -- ` : ` inside a binder when Lean wrapped the signature so the
+        -- top-level `:` sat at end-of-line.  The final binder `(h_d : β = α)`
+        -- ended up rendered as `∀ (w : <conclusion type>` instead.
+        assert.has_match('%(h_d : β = α%)', contents)
+        assert.is_nil(
+          contents:match '∀%s*%(w%s*:%s*∀',
+          ('binder `w` was misparsed:\n%s'):format(contents)
+        )
+
+        hover_win:close()
+        lean_window:make_current()
+      end)
+
       it('falls back to standard hover when RPC fails', function()
         lean_window:make_current()
         helpers.move_cursor { to = { 1, 0 } }