remove ' and add ⟨⟩ in lean autopairs (#10688)

6 months ago · 61818996c6
parent 7e13213e74
commit 61818996c6
1 changed files with 7 additions and 0 deletions
--- 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" }