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

helix-editor · May 5, 2024 · 6181899 · 6181899
1 parent 7e13213
commit 6181899
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" }