From 7a78fb4432fe7aa95e340691ac135dc7e28a9372 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Sun, 29 Dec 2024 18:01:36 -0500
Subject: [PATCH] Make try this replacement not mis-replace on lines with
 unicode.

It's easier to use this lsp helper (which I had previously avoided)
because the char-to-byte-offset stuff is half behind private functions
and I never remember what is actual public API...
---
 lua/lean/widgets.lua           | 12 ++++--------
 spec/infoview/widgets_spec.lua | 29 +++++++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 8 deletions(-)

diff --git a/lua/lean/widgets.lua b/lua/lean/widgets.lua
index d41412dd..e39bad44 100644
--- a/lua/lean/widgets.lua
+++ b/lua/lean/widgets.lua
@@ -120,14 +120,10 @@ implement('Lean.Meta.Tactic.TryThis.tryThisWidget', function(_, props, uri)
           if not vim.api.nvim_buf_is_loaded(bufnr) then
             return
           end
-          vim.api.nvim_buf_set_text(
-            bufnr,
-            props.range.start.line,
-            props.range.start.character,
-            props.range['end'].line,
-            props.range['end'].character,
-            { each.suggestion }
-          )
+
+          ---@type lsp.TextEdit
+          local edit = { range = props.range, newText = each.suggestion }
+          vim.lsp.util.apply_text_edits({ edit }, bufnr, 'utf-16')
 
           local this_infoview = require('lean.infoview').get_current_infoview()
           local this_info = this_infoview and this_infoview.info
diff --git a/spec/infoview/widgets_spec.lua b/spec/infoview/widgets_spec.lua
index 49b487fe..a40e110a 100644
--- a/spec/infoview/widgets_spec.lua
+++ b/spec/infoview/widgets_spec.lua
@@ -77,6 +77,35 @@ describe('widgets', function()
     )
   )
 
+  it(
+    'replaces ranges without being confused by unicode',
+    helpers.clean_buffer(
+      [[
+        example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact?
+      ]],
+      function()
+        helpers.move_cursor { to = { 1, 100 } }
+        assert.infoview_contents.are [[
+          ▶ goals accomplished 🎉
+
+          ▶ suggestion:
+          exact rfl
+
+          ▶ 1:62-1:68: information:
+          Try this: exact rfl
+        ]]
+
+        infoview.go_to()
+        helpers.move_cursor { to = { 4, 1 } }
+        helpers.feed '<CR>'
+
+        assert.contents.are [[
+          example {𝔽 : Type} (x : 𝔽) (_ : 𝔽) (_ : 𝔽) : x = x := by exact rfl
+        ]]
+      end
+    )
+  )
+
   it(
     'supports try this widgets with multiple suggestions',
     helpers.clean_buffer(