Properly indent when we're simultaneously focusing and indenting.

(See the test case.)

Author: Julian

lua/lean/indent.lua

@@ -127,12 +127,12 @@ function M.indentexpr(linenr)
     return last_indent + shiftwidth
   end
 
-  if INDENT_AFTER:match_str(last) then
-    return last_indent + shiftwidth
+  if focuses_at(last, last_indent + 1) then
+    last_indent = last_indent + #'·'
   end
 
-  if focuses_at(last, last_indent + 1) then
-    return last_indent + #'·'
+  if INDENT_AFTER:match_str(last) then
+    return last_indent + shiftwidth
   end
 
   if not is_declaration_args(linenr - 2) then

spec/indent_spec.lua

@@ -254,6 +254,24 @@ describe('indent', function()
     )
   )
 
+  it(
+    'indents again after by at focused stuff',
+    helpers.clean_buffer(
+      [[
+        theorem foo : 37 = 37 := by
+          · have : 37 = 37 := by
+      ]],
+      function()
+        helpers.feed 'Gosorry'
+        assert.contents.are [[
+          theorem foo : 37 = 37 := by
+            · have : 37 = 37 := by
+                sorry
+      ]]
+      end
+    )
+  )
+
   for each in fixtures.indent() do
     it(each.description, function()
       vim.cmd.edit { each.unindented, bang = true }