From daa307ee142ae1e2af4cc2dfd94eb53f99cb3ef2 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:56:06 +0800 Subject: [PATCH] set agda version to unknown before agda-mode:load --- lib/commander.js | 6 +++++- lib/process.js | 2 +- src/commander.ts | 6 +++++- src/process.ts | 2 +- 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/lib/commander.js b/lib/commander.js index 939bad7c..14896bd5 100644 --- a/lib/commander.js +++ b/lib/commander.js @@ -73,7 +73,11 @@ 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', diff --git a/lib/process.js b/lib/process.js index 5c56e6ba..d6ac6457 100644 --- a/lib/process.js +++ b/lib/process.js @@ -106,7 +106,7 @@ var Process = (function () { var path = atom.config.get('agda-mode.executablePath'); var args = _this.getProgramArgs(); args.push('--interaction'); - var agdaVersion = _this.agdaVersion ? _this.agdaVersion.raw : 'null'; + var agdaVersion = _this.agdaVersion ? _this.agdaVersion.raw : 'unknown'; _this.core.view.set('Info', [ ("Agda version: " + agdaVersion), ("Agda executable path: " + path), diff --git a/src/commander.ts b/src/commander.ts index 1d247527..85010e6c 100644 --- a/src/commander.ts +++ b/src/commander.ts @@ -90,7 +90,11 @@ 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', diff --git a/src/process.ts b/src/process.ts index d46badd6..b73912b8 100644 --- a/src/process.ts +++ b/src/process.ts @@ -293,7 +293,7 @@ export default class Process { const path = atom.config.get('agda-mode.executablePath'); const args = this.getProgramArgs(); args.push('--interaction'); - const agdaVersion = this.agdaVersion ? this.agdaVersion.raw : 'null'; + const agdaVersion = this.agdaVersion ? this.agdaVersion.raw : 'unknown'; this.core.view.set('Info', [ `Agda version: ${agdaVersion}`, `Agda executable path: ${path}`,