diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua index 17b6df45..70448173 100644 --- a/lua/lean/indent.lua +++ b/lua/lean/indent.lua @@ -1,19 +1,19 @@ local M = {} -- Borrowed from the (not merged) https://github.com/leanprover/vscode-lean4/pull/329/ -local INDENT_AFTER = vim.regex(([[\<\(%s\)$]]):format(table.concat({ - 'by', - 'do', - 'try', - 'finally', - 'then', - 'else', - 'where', - 'from', - 'extends', - 'deriving', +local INDENT_AFTER = vim.regex(([[\(%s\)$]]):format(table.concat({ + '\\', - ':=', }, [[\|]]))) local NEVER_INDENT = vim.regex(([[^\s*\(%s\)]]):format(table.concat({ 'attribute ', diff --git a/spec/indent_spec.lua b/spec/indent_spec.lua index 126b45af..a13b7196 100644 --- a/spec/indent_spec.lua +++ b/spec/indent_spec.lua @@ -68,6 +68,26 @@ describe('indent', function() ) ) + it( + 'indents after =>', + helpers.clean_buffer( + [[ + example {n : Nat} : n = n := by + induction n with + | zero => + ]], + function() + helpers.feed 'Gorfl' + assert.contents.are [[ + example {n : Nat} : n = n := by + induction n with + | zero => + rfl + ]] + end + ) + ) + it( 'respects shiftwidth', helpers.clean_buffer([[structure foo where]], function()