Don't be indent-confused by from sorry.

Author: Julian

lua/lean/indent.lua

@@ -110,8 +110,11 @@ function M.indentexpr(linenr)
   end
 
   local sorry = sorry_at(linenr - 2, #last - 1)
-  if sorry and not last:find ':=' then
-    return math.max(0, sorry - shiftwidth - 1)
+  if sorry then
+    local before = last:sub(1, sorry)
+    if not before:find ':=%s*' and not before:find 'from%s*' then
+      return math.max(0, sorry - shiftwidth - 1)
+    end
   end
 
   local _, last_indent = last:find '^%s*'

spec/indent_spec.lua

@@ -141,6 +141,24 @@ describe('indent', function()
     )
   )
 
+  it(
+    'is not confused by sorry after from',
+    helpers.clean_buffer(
+      [[
+        example : 37 = 37 := by
+          suffices h : 73 = 73 from sorry
+     ]],
+      function()
+        helpers.feed 'Gorfl'
+        assert.contents.are [[
+          example : 37 = 37 := by
+            suffices h : 73 = 73 from sorry
+            rfl
+      ]]
+      end
+    )
+  )
+
   it(
     'dedents after focused sorry',
     helpers.clean_buffer(