Fix unable to input certain symbols before agda-mode:load

To be specific: '{', '[', '(', '"', '\'', and '`'.
banacorn · Nov 8, 2016 · 9f74907 · 9f74907
1 parent 551cc1f
commit 9f74907
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 2 deletions.
diff --git a/lib/commander.js b/lib/commander.js
diff --git a/src/commander.ts b/src/commander.ts
@@ -90,7 +90,14 @@ export default class Commander {
 
     activate(command: Command) {
         // some commands can only be executed after 'loaded'
-        const exception = ['Load', 'Quit', 'Info', 'InputSymbol'];
+        const exception = ['Load', 'Quit', 'Info', 'InputSymbol',
+                'InputSymbolCurlyBracket',
+                'InputSymbolBracket',
+                'InputSymbolParenthesis',
+                'InputSymbolDoubleQuote',
+                'InputSymbolSingleQuote',
+                'InputSymbolBackQuote'
+            ];
         if(this.loaded || _.includes(exception, command.kind)) {
             this.dispatchCommand(command)
                 .then((result) => {