From 9f74907e57050887cb97c6284bd7566e89b08a57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?T=C3=AEng-Gi=C4=81n=20Lu=C4=81?= Date: Tue, 8 Nov 2016 13:28:30 +0800 Subject: [PATCH] Fix unable to input certain symbols before agda-mode:load To be specific: '{', '[', '(', '"', '\'', and '`'. --- lib/commander.js | 9 ++++++++- src/commander.ts | 9 ++++++++- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/lib/commander.js b/lib/commander.js index 9212e1f3..939bad7c 100644 --- a/lib/commander.js +++ b/lib/commander.js @@ -73,7 +73,14 @@ var Commander = (function () { Commander.prototype.activate = function (command) { var _this = this; // some commands can only be executed after 'loaded' - var exception = ['Load', 'Quit', 'Info', 'InputSymbol']; + var exception = ['Load', 'Quit', 'Info', 'InputSymbol', + 'InputSymbolCurlyBracket', + 'InputSymbolBracket', + 'InputSymbolParenthesis', + 'InputSymbolDoubleQuote', + 'InputSymbolSingleQuote', + 'InputSymbolBackQuote' + ]; if (this.loaded || _.includes(exception, command.kind)) { this.dispatchCommand(command) .then(function (result) { diff --git a/src/commander.ts b/src/commander.ts index 672c6055..1d247527 100644 --- 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) => {