Do not finish input translation on closing braces.

Closes #46.
leanprover · Feb 11, 2020 · 077cb43 · 077cb43
1 parent 3bf3443
commit 077cb43
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/input.ts b/src/input.ts
@@ -166,8 +166,8 @@ class TextEditorAbbrevHandler {
                 } else if (change.text === this.leader) {
                     return this.convertRange(
                         new Range(change.range.start, change.range.start.translate(0, 1)));
-                } else if (change.text.match(/^\s+|[)}⟩]$/)) {
-                    // whitespace, closing parens
+                } else if (change.text.match(/^\s+$/)) {
+                    // whitespace
                     return this.convertRange();
                 }
             }