From f35841403a5b47283d40cb03544aaeebdbd07492 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Mon, 2 Dec 2024 12:39:05 -0500
Subject: [PATCH] Handle another dedent case.

---
 lua/lean/indent.lua                      | 22 ++++++++++++++--------
 spec/fixtures/indent/with_dedent.in.lean |  4 ++++
 spec/fixtures/indent/with_dedent.lean    |  4 ++++
 3 files changed, 22 insertions(+), 8 deletions(-)
 create mode 100644 spec/fixtures/indent/with_dedent.in.lean
 create mode 100644 spec/fixtures/indent/with_dedent.lean

diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua
index 8ac12209..b080da19 100644
--- a/lua/lean/indent.lua
+++ b/lua/lean/indent.lua
@@ -57,22 +57,28 @@ function M.indentexpr(linenr)
   -- 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:gsub('^%s*', '')) then
+  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 vim.bo.shiftwidth
+    return shiftwidth
   elseif last:find ':%s*$' then
-    return vim.bo.shiftwidth * 2
+    return shiftwidth * 2
   elseif last:find ':=%s*$' then
-    return vim.bo.shiftwidth
+    return shiftwidth
   elseif last_indent and focuses_at(last, last_indent + 1) then
     return last_indent + #'·'
   elseif INDENT_AFTER:match_str(last) and not INDENT_AFTER:match_str(current) then
-    return (last_indent or 0) + vim.bo.shiftwidth
+    return (last_indent or 0) + shiftwidth
   elseif last_indent and is_enclosed(linenr - 1) then
-    return last_indent + vim.bo.shiftwidth
-  elseif last_indent and not is_block_comment(linenr - 2) then
-    local dedent_one = last_indent - vim.bo.shiftwidth
+    return last_indent + shiftwidth
+  elseif
+    last_indent
+    and (current_indent == 0 or math.abs(current_indent - last_indent) < shiftwidth)
+    and not is_block_comment(linenr - 2)
+  then
+    local dedent_one = last_indent - shiftwidth
 
     -- We could go backwards to check but that would involve looking back
     -- repetaedly over lines backwards, so we cheat and just check whether the
diff --git a/spec/fixtures/indent/with_dedent.in.lean b/spec/fixtures/indent/with_dedent.in.lean
new file mode 100644
index 00000000..19445e36
--- /dev/null
+++ b/spec/fixtures/indent/with_dedent.in.lean
@@ -0,0 +1,4 @@
+example : 2 = 2 := by
+  have : 2 = 2 := by
+    rfl
+  exact this
diff --git a/spec/fixtures/indent/with_dedent.lean b/spec/fixtures/indent/with_dedent.lean
new file mode 100644
index 00000000..19445e36
--- /dev/null
+++ b/spec/fixtures/indent/with_dedent.lean
@@ -0,0 +1,4 @@
+example : 2 = 2 := by
+  have : 2 = 2 := by
+    rfl
+  exact this