Skip to content

Commit

Permalink
Properly indent after =>.
Browse files Browse the repository at this point in the history
I'm being lazy and not investigating why it doesn't match
the word boundary...
  • Loading branch information
Julian committed Dec 24, 2024
1 parent bda928a commit b8c8a33
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 12 deletions.
24 changes: 12 additions & 12 deletions lua/lean/indent.lua
Original file line number Diff line number Diff line change
@@ -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({
'\\<by',
'\\<do',
'\\<try',
'\\<finally',
'\\<then',
'\\<else',
'\\<where',
'\\<from',
'\\<extends',
'\\<deriving',
'\\<:=',
'=>',
':=',
}, [[\|]])))
local NEVER_INDENT = vim.regex(([[^\s*\(%s\)]]):format(table.concat({
'attribute ',
Expand Down
20 changes: 20 additions & 0 deletions spec/indent_spec.lua
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down

0 comments on commit b8c8a33

Please sign in to comment.