Inside multiline delimiters redux.

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
 

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"]

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"]

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 }

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