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

smortime · Jul 10, 2024 · 0885ae3 · 0885ae3
1 parent 995049e
commit 0885ae3
Showing 1 changed file with 7 additions and 0 deletions.
diff --git 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" }