From 1da3354345f4873a3af3e72bb436547f28a90e24 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Sat, 11 Jan 2025 09:02:09 -0500 Subject: [PATCH] Back out the structure literal syntax separation. It breaks syntax highlighting for string interpolation, and I spent like 2 hours trying to figure out why adding `leanStringInterpolation` to the `containedin=ALLBUT` doesn't fix it, but it doesn't. We don't need this anymore for indent, so, go away. --- syntax/lean.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/lean.vim b/syntax/lean.vim index de697255..1a47b18d 100644 --- a/syntax/lean.vim +++ b/syntax/lean.vim @@ -66,9 +66,9 @@ syn region leanEncl matchgroup=leanDelim start="#\[" end="\]" contains=TOP conta syn region leanEncl matchgroup=leanDelim start="(" end=")" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend syn region leanEncl matchgroup=leanDelim start="\[" end="\]" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend syn region leanEncl matchgroup=leanDelim start="⦃" end="⦄" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend +syn region leanEncl matchgroup=leanDelim start="⟨" end="⟩" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend syn region leanAnonymousLiteral matchgroup=leanDelim start="⟨" end="⟩" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend -syn region leanStructureLiteral matchgroup=leanDelim start="{" end="}" contains=TOP containedin=ALLBUT,leanBlockComment,leanComment,leanFrenchQuote keepend " FIXME(gabriel): distinguish backquotes in notations from names " syn region leanNotation start=+`+ end=+`+