diff --git a/lua/lean/indent.lua b/lua/lean/indent.lua index ecc04a54..1e07719a 100644 --- a/lua/lean/indent.lua +++ b/lua/lean/indent.lua @@ -52,10 +52,12 @@ end ---Is the given line within a Lean enclosed bracket? ---@param linenr number +---@param position integer ---@return boolean -local function is_enclosed(linenr) - local syntax = vim.inspect_pos(0, linenr, 0).syntax[1] - return syntax and syntax.hl_group == 'leanEncl' +local function is_enclosed(linenr, position) + local syntax = vim.inspect_pos(0, linenr, position).syntax[1] + local hlgroup = syntax and syntax.hl_group + return hlgroup == 'leanEncl' or hlgroup == 'leanAnonymousLiteral' end ---Is the given line within a Lean comment (normal or block)? @@ -110,16 +112,18 @@ function M.indentexpr(linenr) local _, last_indent = last:find '^%s+' + if is_enclosed(linenr - 1, 0) then + if is_enclosed(linenr - 2, 0) then + return last_indent + end + return (last_indent or 0) + shiftwidth + end + if last_indent then if focuses_at(last, last_indent + 1) then return last_indent + #'·' end - if is_enclosed(linenr - 1) then - local _, bracket = last:find '%[' - return bracket or last_indent + shiftwidth - end - if not is_declaration_args(linenr - 2) then local dedent_one = last_indent - shiftwidth diff --git a/spec/fixtures/indent/multiline_delimited.in.lean b/spec/fixtures/indent/multiline_delimited.in.lean new file mode 100644 index 00000000..da2f1c5f --- /dev/null +++ b/spec/fixtures/indent/multiline_delimited.in.lean @@ -0,0 +1,14 @@ +def f := "foo bar +baz +quux" + +def g := [1, 2, +3, +4, +5] + +def h := [1, 2, +3] + +def i := ["foo", "bar", +"baz"] diff --git a/spec/fixtures/indent/multiline_delimited.lean b/spec/fixtures/indent/multiline_delimited.lean new file mode 100644 index 00000000..cd308399 --- /dev/null +++ b/spec/fixtures/indent/multiline_delimited.lean @@ -0,0 +1,14 @@ +def f := "foo bar +baz +quux" + +def g := [1, 2, + 3, + 4, + 5] + +def h := [1, 2, + 3] + +def i := ["foo", "bar", + "baz"] diff --git a/spec/indent_spec.lua b/spec/indent_spec.lua index 9bb0c17d..b8c56daa 100644 --- a/spec/indent_spec.lua +++ b/spec/indent_spec.lua @@ -135,24 +135,6 @@ describe('indent', function() ) ) - it( - 'aligns with brackets', - helpers.clean_buffer( - [[ - example : 37 = 37 ∧ 73 = 73 := by - simp [Nat.lt_or_gt, - ]], - function() - helpers.feed 'GoNat.lt_or_gt]' - assert.contents.are [[ - example : 37 = 37 ∧ 73 = 73 := by - simp [Nat.lt_or_gt, - Nat.lt_or_gt] - ]] - end - ) - ) - for each in fixtures.indent() do it(each.description, function() vim.cmd.edit { each.unindented, bang = true } diff --git a/syntax/lean.vim b/syntax/lean.vim index 1d75de12..634fb273 100644 --- a/syntax/lean.vim +++ b/syntax/lean.vim @@ -66,8 +66,8 @@ syn region leanEncl matchgroup=leanDelim start="#\[" end="\]" contains=TOP conta syn region leanEncl matchgroup=leanDelim start="(" end=")" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend syn region leanEncl matchgroup=leanDelim start="\[" end="\]" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend syn region leanEncl matchgroup=leanDelim start="⦃" end="⦄" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend -syn region leanEncl matchgroup=leanDelim start="⟨" end="⟩" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend +syn region leanAnonymousLiteral matchgroup=leanDelim start="⟨" end="⟩" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend syn region leanStructureLiteral matchgroup=leanDelim start="{" end="}" contains=TOP containedin=ALLBUT,leanFrenchQuote keepend " FIXME(gabriel): distinguish backquotes in notations from names