Skip to content
This repository has been archived by the owner on Feb 26, 2021. It is now read-only.

Commit

Permalink
set agda version to unknown before agda-mode:load
Browse files Browse the repository at this point in the history
  • Loading branch information
banacorn committed Nov 8, 2016
1 parent 9f74907 commit daa307e
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 4 deletions.
6 changes: 5 additions & 1 deletion lib/commander.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion lib/process.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 5 additions & 1 deletion src/commander.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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',
Expand Down
2 changes: 1 addition & 1 deletion src/process.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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}`,
Expand Down

0 comments on commit daa307e

Please sign in to comment.