From 40256d19f5c2dc5aa640ec687967bfc8bd4aa92d Mon Sep 17 00:00:00 2001 From: Ashley Vaughn <59515175+ashl3y-v@users.noreply.github.com> Date: Sun, 5 May 2024 06:48:50 -0700 Subject: [PATCH] =?UTF-8?q?remove=20'=20and=20add=20=E2=9F=A8=E2=9F=A9=20i?= =?UTF-8?q?n=20lean=20autopairs=20(#10688)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- languages.toml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/languages.toml b/languages.toml index ecf1b49fd0407..ec3e36ed67b89 100644 --- a/languages.toml +++ b/languages.toml @@ -1040,6 +1040,13 @@ block-comment-tokens = { start = "/-", end = "-/" } language-servers = [ "lean" ] indent = { tab-width = 2, unit = " " } +[language.auto-pairs] +'(' = ')' +'{' = '}' +'[' = ']' +'"' = '"' +'⟨' = '⟩' + [[grammar]] name = "lean" source = { git = "https://github.com/Julian/tree-sitter-lean", rev = "d98426109258b266e1e92358c5f11716d2e8f638" }