Add support for Lean 4.24's try this widget.

Even though it's about to change again in leanprover/lean4#10524...

Author: Julian

lua/lean/widgets/Lean/Meta/Hint/tryThisDiffWidget.lua

@@ -0,0 +1,40 @@
+---@brief [[
+--- The `Try This` widget on versions of Lean v4.24+.
+---@brief ]]
+
+local Element = require('lean.tui').Element
+
+---@alias SuggestionText string
+
+---@class TryThis.Suggestion
+---@field suggestion SuggestionText Text to be used as a replacement via a code action.
+---@field preInfo? string Optional info to be printed immediately before replacement text in a widget.
+---@field postInfo? string Optional info to be printed immediately after replacement text in a widget.
+
+---A code action suggestion associated with a hint in a message.
+---
+---Refer to `TryThis.Suggestion`. This extends that structure with several fields specific to inline
+---hints.
+---@class Suggestion: TryThis.Suggestion
+
+---@class TryThisParams
+---@field diff { type: 'insertion' | 'deletion' | 'unchanged', text: string }[]
+---@field range lsp.Range
+---@field suggestion string
+
+---@param ctx RenderContext
+---@param props TryThisParams
+return function(ctx, props)
+  return Element:new {
+    text = props.suggestion,
+    highlightable = true,
+    hlgroup = 'widgetLink',
+    events = {
+      click = function()
+        ctx:apply_edits {
+          { range = props.range, newText = props.suggestion },
+        }
+      end,
+    },
+  }
+end

lua/lean/widgets/Lean/Meta/Tactic/TryThis/tryThisWidget.lua

@@ -1,21 +1,18 @@
-local Element = require('lean.tui').Element
-
----@alias SuggestionText string
+---@brief [[
+--- The `Try This` widget on old versions of Lean pre-v4.23.
+---@brief ]]
 
----@class Suggestion
----@field suggestion SuggestionText Text to be used as a replacement via a code action.
----@field preInfo? string Optional info to be printed immediately before replacement text in a widget.
----@field postInfo? string Optional info to be printed immediately after replacement text in a widget.
+local Element = require('lean.tui').Element
 
----@class TryThisParams
----@field suggestions Suggestion[]
+---@class LegacyTryThisParams
+---@field suggestions TryThis.Suggestion[]
 ---@field range lsp.Range
 ---@field header string
 ---@field isInline boolean
 ---@field style any
 
 ---@param ctx RenderContext
----@param props TryThisParams
+---@param props LegacyTryThisParams
 return function(ctx, props)
   local blocks = vim.iter(ipairs(props.suggestions)):map(function(i, each)
     local children = {

spec/widgets/core_spec.lua

@@ -2,12 +2,16 @@
 --- Tests for widgets from Lean core.
 ---@brief ]]
 
+local Window = require 'std.nvim.window'
+
 local helpers = require 'spec.helpers'
 local infoview = require 'lean.infoview'
 
 require('lean').setup {}
 
 describe('Lean core widgets', function()
+  local lean_window = Window:current()
+
   it(
     'supports error description widgets',
     helpers.clean_buffer('def f := g', function()
@@ -35,18 +39,17 @@ describe('Lean core widgets', function()
 
           ⊢ 2 = 2
 
-          ▼ suggestion:
-          exact rfl
-
           ▼ 2:3-2:9: information:
-          Try this: exact rfl
+          Try this:
+            exact rfl
         ]]
 
         infoview.go_to()
-        helpers.move_cursor { to = { 6, 1 } }
+        helpers.search 'exact '
         helpers.feed '<CR>'
 
         -- the buffer contents have changed but we also jumped to the lean win
+        assert.current_window.is(lean_window)
         assert.contents.are [[
           example : 2 = 2 := by
             exact rfl
@@ -66,17 +69,16 @@ describe('Lean core widgets', function()
         assert.infoview_contents.are [[
           Goals accomplished 🎉
 
-          ▼ suggestion:
-          exact rfl
-
           ▼ 1:62-1:68: information:
-          Try this: exact rfl
+          Try this:
+            exact rfl
         ]]
 
         infoview.go_to()
-        helpers.move_cursor { to = { 4, 1 } }
+        helpers.search 'exact '
         helpers.feed '<CR>'
 
+        assert.current_window.is(lean_window)
         assert.contents.are [[
           example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact rfl
         ]]
@@ -105,14 +107,10 @@ describe('Lean core widgets', function()
         assert.infoview_contents.are [[
           ⊢ True
 
-          ▼ suggestion:
-          trivial
-          sorry
-
           ▼ 11:3-11:6: information:
           Try these:
-          • trivial
-          • sorry
+            • trivial
+            • sorry
         ]]
       end
     )
@@ -140,17 +138,13 @@ describe('Lean core widgets', function()
         assert.infoview_contents.are [[
           ⊢ 37 = 37
 
-          ▼ suggestion:
-          trivial
-
-          ▼ suggestion:
-          rfl
-
           ▼ 10:25-10:39: information:
-          Try this: trivial
+          Try this:
+            trivial
 
           ▼ 10:25-10:39: information:
-          Try this: rfl
+          Try this:
+            rfl
 
           ▼ 10:22-10:39: error:
           unsolved goals