From e9ba280db9765e8bbd5c5347841f959da20d24b1 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Fri, 13 Dec 2024 03:04:13 -0500
Subject: [PATCH] And another...

---
 lua/lean/indent.lua                        | 14 ++++++++------
 spec/fixtures/indent/nested_indent.in.lean |  7 +++++++
 spec/fixtures/indent/nested_indent.lean    |  7 +++++++
 3 files changed, 22 insertions(+), 6 deletions(-)
 create mode 100644 spec/fixtures/indent/nested_indent.in.lean
 create mode 100644 spec/fixtures/indent/nested_indent.lean

diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua
index 8f379714..20f5fa72 100644
--- a/lua/lean/indent.lua
+++ b/lua/lean/indent.lua
@@ -52,17 +52,21 @@ function M.indentexpr(linenr)
   end
 
   local last, current = unpack(vim.api.nvim_buf_get_lines(0, linenr - 2, linenr, true))
+  local shiftwidth = vim.bo.shiftwidth
+
+  local _, current_indent = current:find '^%s*'
+  if current_indent > 0 and current_indent < #current and current_indent % shiftwidth == 0 then
+    return current_indent
+  end
 
   -- Lua patterns are... seemingly broken with unicode and/or multibyte
   -- characters. Specifically `('  foo'):find '^(%s+)([z]?)(.*)'` works fine to
   -- match an optional `z`, but ('  foo'):find '^(%s+)([·]?)(.*)' does not.
   local _, last_indent = last:find '^%s+'
-  local _, current_indent = current:find '^%s*'
-  local shiftwidth = vim.bo.shiftwidth
 
   if focuses_at(current, current_indent + 1) then
-    -- FIXME this seems wrong, and needs to check if the previous line is focused or not
-    return shiftwidth
+    local last_was_focused = (last_indent or 0) % shiftwidth == #'·'
+    return last_was_focused and (last_indent - #'· ') or last_indent + shiftwidth
   elseif last:find ':%s*$' then
     return shiftwidth * 2
   elseif last:find ':=%s*$' then
@@ -71,8 +75,6 @@ function M.indentexpr(linenr)
     return last_indent + #'·'
   elseif last_indent and is_enclosed(linenr - 1) then
     return last_indent + shiftwidth
-  elseif current_indent and current_indent > 0 and current_indent % shiftwidth == 0 then
-    return current_indent
   elseif last_indent and not is_block_comment(linenr - 2) then
     local dedent_one = last_indent - shiftwidth
 
diff --git a/spec/fixtures/indent/nested_indent.in.lean b/spec/fixtures/indent/nested_indent.in.lean
new file mode 100644
index 00000000..a46e79ed
--- /dev/null
+++ b/spec/fixtures/indent/nested_indent.in.lean
@@ -0,0 +1,7 @@
+def foo : X where
+  bar := by
+    apply foo_bar
+    · rw [bar]
+      sorry
+    · rw [bar]
+      sorry
diff --git a/spec/fixtures/indent/nested_indent.lean b/spec/fixtures/indent/nested_indent.lean
new file mode 100644
index 00000000..a46e79ed
--- /dev/null
+++ b/spec/fixtures/indent/nested_indent.lean
@@ -0,0 +1,7 @@
+def foo : X where
+  bar := by
+    apply foo_bar
+    · rw [bar]
+      sorry
+    · rw [bar]
+      sorry