idris-hackers / atom-language-idris Goto Github PK

View Code? Open in Web Editor NEW

100.0 100.0 24.0 438 KB

A Idris Mode for Atom.io

License: MIT License

CoffeeScript 7.50% TypeScript 91.64% Less 0.86%

atom-language-idris's People

Contributors

Stargazers

Watchers

atom-language-idris's Issues

Uncaught Error: Can't save buffer with no file path

Create a new buffer.
Set its grammar to idris-language.
Invoke the typecheck command, as suggested in https://github.com/idris-hackers/atom-language-idris/blob/master/documentation/tutorial.md.

A few fixes come to mind:

Disable that command for unsaved buffers (not sure atom lets you do this)
Present a dialog to the user to tell them "save first"
Save to a temp file and typecheck that (the save becomes transparent to the user, and the buffer is still not tied to a file on disk)

Atom Version: 1.0.5
System: Mac OS X 10.10.4
Thrown From: language-idris package, v0.2.1

Stack Trace

Uncaught Error: Can't save buffer with no file path

At /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/text-buffer/lib/text-buffer.js:998

Error: Can't save buffer with no file path
  at TextBuffer.module.exports.TextBuffer.saveAs (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/text-buffer/lib/text-buffer.js:998:15)
  at TextBuffer.module.exports.TextBuffer.save (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/text-buffer/lib/text-buffer.js:992:19)
  at TextEditor.module.exports.TextEditor.save (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/text-editor.js:579:26)
  at IdrisController.typecheckFile (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:53:18)
  at /Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at atom-text-editor.<anonymous> (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:48:9)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at CommandPaletteView.module.exports.CommandPaletteView.confirmed (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/command-palette/lib/command-palette-view.js:159:32)
  at CommandPaletteView.module.exports.SelectListView.confirmSelection (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:338:21)
  at space-pen-div.atom.commands.add.core:confirm (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:109:19)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at KeymapManager.module.exports.KeymapManager.dispatchCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:524:16)
  at KeymapManager.module.exports.KeymapManager.handleKeyboardEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:347:22)
  at HTMLDocument.module.exports.WindowEventHandler.onKeydown (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/window-event-handler.js:177:20)

Commands

     -0:23.6.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:20.2.0 core:move-down (atom-text-editor.editor.mini.is-focused)
     -0:19.8.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:19.8.0 language-idris:typecheck (atom-text-editor.editor)
     -0:11.3.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:08.0 core:backspace (atom-text-editor.editor.mini.is-focused)
     -0:06.6.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:06.6.0 language-idris:typecheck (atom-text-editor.editor)

Config

{
  "core": {
    "themes": [
      "atom-material-ui",
      "atom-material-syntax"
    ]
  },
  "language-idris": {
    "pathToIdris": "/usr/local/bin/idris"
  }
}

Installed Packages

# User
atom-material-syntax, v0.2.1
atom-material-ui, v0.5.13
autocomplete-haskell, v0.4.5
haskell-ghc-mod, v0.8.8
ide-haskell, v0.7.1
language-haskell, v1.3.0
language-idris, v0.2.1

# Dev
No dev packages

Failed to activate the language-idris package

Hi! I get an error when trying to install this plugin. I guess, it's just because of the atom API changes, but don't know how to fix it.

Atom Version: 0.189.0
System: Mac OS X 10.10.3
Thrown From: language-idris package, v0.0.1

Stack Trace

Failed to activate the language-idris package

At undefined is not a function

TypeError: undefined is not a function
  at IdrisController.init (/Users/laughedelic/.atom/packages/language-idris/lib/idris-controller.js:57:20)
  at new IdrisController (/Users/laughedelic/.atom/packages/language-idris/lib/idris-controller.js:10:8)
  at Object.module.exports.activate (/Users/laughedelic/.atom/packages/language-idris/lib/language-idris.js:13:23)
  at Package.module.exports.Package.activateNow (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/package.js:240:19)
  at /opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/package.js:221:30
  at Package.module.exports.Package.measure (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/package.js:167:15)
  at Package.module.exports.Package.activate (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/package.js:214:14)
  at PackageManager.module.exports.PackageManager.activatePackage (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/package-manager.js:461:21)
  at /opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/node_modules/settings-view/lib/package-manager.js:268:29
  at exit (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/node_modules/settings-view/lib/package-manager.js:43:16)
  at BufferedProcess.triggerExitCallback (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/buffered-process.js:63:47)
  at /opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/buffered-process.js:77:18
  at Socket.<anonymous> (/opt/homebrew-cask/Caskroom/atom/latest/Atom.app/Contents/Resources/app/src/buffered-process.js:150:18)
  at emitOne (events.js:82:20)
  at Socket.emit (events.js:166:7)
  at Pipe.close (net.js:464:12)

Commands

     -0:27.9 command-palette:toggle (atom-text-editor.editor.vim-mode.command-mode)
     -0:24.2 editor:consolidate-selections (atom-text-editor.editor.mini)
     -0:24.2 core:cancel (atom-text-editor.editor.mini)
     -0:23.6 settings-view:open (atom-text-editor.editor.vim-mode.command-mode)
     -0:19.2 core:confirm (atom-text-editor.editor.mini)

The ide-mode closes when the idris code contains an error

the ide-mode closes when the idris code contains an error

Minimal example:

module Test

a

Add a REPL

ide-mode should make this easy.
http://docs.idris-lang.org/en/latest/reference/ide-protocol.html#protocol-overview (:interpret STRING)

the only thing we have to think about is how to display the repl

Ideas:
TextEditorView with mini: true gives an input
https://www.npmjs.com/package/atom-space-pen-views#constructor-params

Better error messages for #23

differentiate at least between the idris executable can't be found and the compiler crashed

ipkg branch: Show holes is empty, Add Clause shows error

I'm on the ipkg-branch (commit 26f6b82 to be exact) and even when typechecking does find all modules now, I have some other trouble, I didn't had on release:

When trying to add a clause I get a pane labeled "Idris Errors". The contentarea of the pane is ": openFile: does not exist (No such file or directory)".
When I try to use the show holes function, I get a pane labeled "Idris: Holes". Contentarea shows just a darkgray background. Just as release looks like, but without anything written into the box.

This happens as well when I am in a directory with an ipkg file as well as without.

Minimal example that shows the problem I have:

module Foo

import Data.Vect

bar : Vect n a -> Vect m a -> Vect (n + m) a
--bar xs ys = ?bar_rhs

I'd expect that something similar to the commented line would be created when using add clause. Also when uncommenting it, I'd expect to see typeinfo about ?bar_rhs in the bottom pane.

Also I am using Idris from git, currently it is (exactly that binary is also configured in atom):

$ /home/nobbz/projects/idris-source/.cabal-sandbox/bin/idris --version
0.9.18.1-git:8205c13

But I don't think idris version should be an issue, it did work before with latest release.

Uncaught Error: Notification must be created with string message: undefined

After the latest update - 0.2.1, this error occurs when I execute typechecking.

Atom Version: 1.0.5
System: Microsoft Windows 10 Pro
Thrown From: language-idris package, v0.2.1

Stack Trace

Uncaught Error: Notification must be created with string message: undefined

At D:\Users\NightRa\AppData\Local\atom\app-1.0.5\resources\app.asar\src\notification.js:25

Error: Notification must be created with string message: undefined
    at Notification.module.exports.Notification.validate (D:\Users\NightRa\AppData\Local\atom\app-1.0.5\resources\app.asar\src\notification.js:25:15)
    at new Notification (D:\Users\NightRa\AppData\Local\atom\app-1.0.5\resources\app.asar\src\notification.js:20:12)
    at NotificationManager.module.exports.NotificationManager.addError (D:\Users\NightRa\AppData\Local\atom\app-1.0.5\resources\app.asar\src\notification-manager.js:41:35)
    at IdrisIdeMode.stopped (D:\Users\NightRa\.atom\packages\language-idris\lib\idris-ide-mode.coffee:64:26)
    at ChildProcess.<anonymous> (D:\Users\NightRa\.atom\packages\language-idris\lib\idris-ide-mode.coffee:3:61)
    at emitTwo (events.js:87:13)
    at ChildProcess.emit (events.js:169:7)
    at Process.ChildProcess._handle.onexit (child_process.js:1057:12)

Commands

     -0:05.7.0 atom-terminal-panel:toggle-autocompletion (atom-text-editor.editor.is-focused)
     -0:05.3.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:03.6.0 core:move-down (atom-text-editor.editor.mini.is-focused)
     -0:03.2.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:03.2.0 language-idris:typecheck (atom-text-editor.editor)

Config

{
  "core": {
    "themes": [
      "one-dark-ui",
      "solarized-dark-syntax"
    ]
  },
  "language-idris": {}
}

Installed Packages

# User
atom-terminal-panel, v4.4.4
autocomplete-haskell, v0.4.5
haskell-ghc-mod, v0.8.8
ide-haskell, v0.7.1
language-haskell, v1.3.0
language-idris, v0.2.1
language-scala, v1.1.3

# Dev
No dev packages

Broken on Windows?

Hi, I'm on Windows. Every time it starts up it asks me to set the path to Idris.

I set the path in the settings AND in the PATH environment variable but it still keeps asking to me to set the path.

I am using the Idris pre complied for Windows downloaded from here https://github.com/idris-lang/Idris-dev/wiki/Windows-Binaries for Windows 64 bit.

Warn user if the idris path points to a directory

Warn user if the idris path points to a directory.
Maybe with a warning that says:
"The path should point to the idris executable and not the folder containing it"

see #71

Pass options to idris executable

Occasionally, I would find it useful to be able to pass arbitrary flags to Idris from Atom, e.g. to turn off the coverage checker or to set language options like --typeintype. Occasionally it would even be nice to add packages with -p, for small demonstration examples where making an ipkg would be overkill.

Is it possible to do this, perhaps just via the settings?

Disable invoking the compiler (optionally)

Please add an option to disable this. It lags out my editing, it currently is crashing every time I open an Idris file, and sometimes all I really want is syntax highlighting. Simply not setting the path to idris isn't good enough, since Atom warns me every time I open it to set the path.

Backslashes not properly unescaped after proof search

The Idris compiler is assigning dumb names to things, like __pi_arg, but aside from that, the Atom mode is also not properly unescaping strings coming from Idris:

When I start with this file:

module AtomTest


foo : Nat -> Nat -> Nat
foo = ?lkj

and invoke proof search on the metavariable ?lkj, I get:

module AtomTest


foo : Nat -> Nat -> Nat
foo = \\__pi_arg => \\__pi_arg1 => (__pi_arg1)

Note the double-backslashes, which should be single backslashes. This is because backslash is used as a string-escaper in the IDE protcol, allowing things like quotes to be included in strings.

IPKG: add commands like idris --build after merging the ipkg branch

Error on startup: Uncaught TypeError: Cannot read property 'stdin' of undefined

When I start Atom with an Idris file open, I get the following error:

Uncaught TypeError: Cannot read property 'stdin' of undefined
/home/davidc/.atom/packages/language-idris/lib/idris-model.coffee:105
Hide Stack Trace
TypeError: Cannot read property 'stdin' of undefined
  at IdrisModel.sendCommand (/home/davidc/.atom/packages/language-idris/lib/idris-model.coffee:105:13)
  at IdrisModel.prepareCommand (/home/davidc/.atom/packages/language-idris/lib/idris-model.coffee:111:6)
  at IdrisModel.load (/home/davidc/.atom/packages/language-idris/lib/idris-model.coffee:114:6)
  at IdrisController.loadFile (/home/davidc/.atom/packages/language-idris/lib/idris-controller.coffee:100:12)
  at IdrisController.paneChanged (/home/davidc/.atom/packages/language-idris/lib/idris-controller.coffee:82:10)
  at /home/davidc/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at Emitter.module.exports.Emitter.emit (/usr/share/atom/resources/app.asar/node_modules/event-kit/lib/emitter.js:82:11)
  at /usr/share/atom/resources/app.asar/src/pane-container.js:343:34
  at Emitter.module.exports.Emitter.emit (/usr/share/atom/resources/app.asar/node_modules/event-kit/lib/emitter.js:82:11)
  at Pane.module.exports.Pane.setActiveItem (/usr/share/atom/resources/app.asar/src/pane.js:234:22)
  at Pane.module.exports.Pane.activateItem (/usr/share/atom/resources/app.asar/src/pane.js:298:21)
  at tabs-tab.<anonymous> (/usr/share/atom/resources/app.asar/node_modules/tabs/lib/tab-bar-view.js:159:24)
  at space-pen-ul.jQuery.event.dispatch (/usr/share/atom/resources/app.asar/node_modules/jquery/dist/jquery.js:4435:9)
  at space-pen-ul.elemData.handle (/usr/share/atom/resources/app.asar/node_modules/jquery/dist/jquery.js:4121:28)

This is on Ubuntu 15.04 running the latest Atom and the latest language-idris release from the settings window.

Syntax: ' in the end of string should not be highlighted as quote

for example index' doesn't open quote but highlighting will fail on it

Uncaught Error: spawn EACCES

Any Idris command (Typechecking in this case)

Atom Version: 1.0.19
System: Mac OS X 10.10.5
Thrown From: language-idris package, v0.3.3

Stack Trace

Uncaught Error: spawn EACCES

At /Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:549

Error: spawn EACCES
  at exports._errnoException (util.js:814:11)
  at ChildProcess.spawn (internal/child_process.js:298:11)
  at exports.spawn (child_process.js:343:9)
  at IdrisIdeMode.start (/Users/sgraf/.atom/packages/language-idris/lib/idris-ide-mode.coffee:38:9)
  at IdrisModel.ideMode (/Users/sgraf/.atom/packages/language-idris/lib/idris-model.coffee:19:19)
  at IdrisModel.prepareCommand (/Users/sgraf/.atom/packages/language-idris/lib/idris-model.coffee:73:6)
  at IdrisModel.interpret (/Users/sgraf/.atom/packages/language-idris/lib/idris-model.coffee:113:6)
  at IdrisModel.changeDirectory (/Users/sgraf/.atom/packages/language-idris/lib/idris-model.coffee:77:6)
  at IdrisModel.load (/Users/sgraf/.atom/packages/language-idris/lib/idris-model.coffee:89:10)
  at IdrisController.typecheckFile (/Users/sgraf/.atom/packages/language-idris/lib/idris-controller.coffee:86:8)
  at /Users/sgraf/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at AnonymousObserver._onNext (/Users/sgraf/.atom/packages/language-idris/lib/idris-controller.coffee:63:11)
  at AnonymousObserver.Rx.AnonymousObserver.AnonymousObserver.next (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1811:12)
  at AnonymousObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
  at AnonymousObserver.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
  at InnerObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:3092:90)
  at InnerObserver.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
  at scheduleItem (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:2566:16)
  at Scheduler.scheduleNow [as _schedule] (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1173:50)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:957:19)
  at JustSink.run (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:2571:36)
  at JustObservable.subscribeCore (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:2556:19)
  at JustObservable.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at [object Object].setDisposable [as action] (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1984:46)
  at [object Object].ScheduledItem.invokeCore (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:916:17)
  at [object Object].ScheduledItem.invoke (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:904:40)
  at runTrampoline (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1186:37)
  at tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at Scheduler.scheduleNow [as _schedule] (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1197:45)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:957:19)
  at JustObservable.subscribe [as _subscribe] (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1996:32)
  at JustObservable.Rx.Observable.observableProto.subscribe.observableProto.forEach (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1873:19)
  at MergeAllObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:3060:37)
  at MergeAllObserver.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
  at MapObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:3862:19)
  at MapObserver.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
  at AsyncSubject.Rx.AsyncSubject.addProperties.onCompleted (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5631:17)
  at AsyncSubject.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1763:14)
  at AutoDetachObserver.tryCatcher (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1763:14)
  at handler (/Users/sgraf/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:4223:20)
  at FSReqWrap.oncomplete (fs.js:82:15)

Commands

  7x -3:15.4.0 vim-mode:move-up (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
  2x -3:13.7.0 vim-mode:move-to-next-word (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
  3x -3:13.1.0 vim-mode:move-down (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
 13x -3:12.4.0 vim-mode:move-up (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
  9x -3:10.4.0 vim-mode:move-down (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
  3x -3:09.0 vim-mode:move-to-next-word (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -3:08.0 vim-mode:move-down (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -3:07.5.0 vim-mode:activate-insert-mode (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -3:06.1.0 vim-mode:activate-normal-mode (atom-text-editor.editor.vim-mode.is-focused.insert-mode)
 12x -3:05.9.0 vim-mode:move-down (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -3:03.8.0 vim-mode:activate-insert-mode (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -3:02.4.0 vim-mode:activate-normal-mode (atom-text-editor.editor.vim-mode.is-focused.insert-mode)
     -3:01.7.0 core:save (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -2:58.9.0 pane:show-next-item (atom-text-editor.editor.vim-mode.is-focused.normal-mode)
     -2:57.4.0 pane:show-previous-item (div.settings-view.pane-item)
  2x -2:56.3.0 language-idris:typecheck (atom-text-editor.editor.vim-mode.normal-mode.is-focused)

Config

{
  "core": {},
  "language-idris": {
    "pathToIdris": "/Users/sgraf/.cabal/bin"
  }
}

Installed Packages

# User
autocomplete-haskell, v0.5.1
haskell-ghc-mod, v0.9.12
language-elm, v1.0.3
language-haskell, v1.4.9
language-idris, v0.3.3
minimap, v4.13.4
sync-settings, v0.6.0
vim-mode, v0.60.0

# Dev
No dev packages

TypeError when trying to load an empty file

I’m trying to open an empty .idr file I’ve just created, but language-idris is throwing a TypeError:

Starting Idris IDESlave /Users/rob/.atom/packages/language-idris/lib/idris-controller.js:72
Loading /Users/rob/Desktop/bezier.idr /Users/rob/.atom/packages/language-idris/lib/idris-controller.js:140
Exited /Users/rob/.atom/packages/language-idris/lib/idris-model.js:100
Loading /Users/rob/Desktop/bezier.idr /Users/rob/.atom/packages/language-idris/lib/idris-controller.js:140
Uncaught TypeError: Cannot read property 'stdin' of undefined /Users/rob/.atom/packages/language-idris/lib/idris-model.js:115

Status message should appear only in idris projects

When I open whatever project not related to idris, I see the message Idris (Not loaded) in the status bar, which doesn't make any sense in this context:

Add autocompletion

the ide-mode can provide completion. Use it together with http://blog.atom.io/2015/05/15/new-autocomplete.html.

First experimentations here: https://github.com/idris-hackers/atom-language-idris/tree/autocomplete-tests

Can't figure out how to install and use

I've been wanting to follow along in the development of this package, but I can't seem to figure it out. I'm completely new to Atom, so please take this in that spirit.

When I do "apm install", Atom doesn't seem to actually get a copy of the plugin. I've also tried symlinking the repo into ~/.atom/packages/language-idris, but then it shows up as a very old version with a picture of @fangel's face, rather than showing the metadata in the JSON file in the repo.

I can get into a settings window and give it the path to Idris, but none of the keyboard shortcuts in the README seem to work - I certainly don't see anything happen, though I may just not know what to look for.

I don't know how much of this is my not knowing Atom, and how much is the plugin. However, this plugin does have the potential to be the "goto Idris interface" for people who aren't in to the classical editors, so it might be nice to have documentation on how to install it and set it up, and perhaps a short tutorial saying "paste in add : Nat -> Nat -> Nat, then do this to add a clause, then this to case split, then fill it out, then type check with this command". Another thing that's been nice in idris-mode for Emacs has been having a menu that lists the available commands, for those haven't yet learned keybindings.

I keep seeing tantalizing screenshots, but the package has, thus far, eluded me.

Uncaught ReferenceError: editor is not defined

Reproduce:

Attempting to use "Showing the types of meta-variables (ctrl-alt-t)" on any position

Atom Version: 1.0.5
System: Mac OS X 10.10.4
Thrown From: language-idris package, v0.2.3

Stack Trace

Uncaught ReferenceError: editor is not defined

At /Users/hannes/.atom/packages/language-idris/lib/idris-controller.coffee:95

ReferenceError: editor is not defined
  at IdrisController.getTypeForWord (/Users/hannes/.atom/packages/language-idris/lib/idris-controller.coffee:95:11)
  at /Users/hannes/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at atom-text-editor.<anonymous> (/Users/hannes/.atom/packages/language-idris/lib/idris-controller.coffee:51:9)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/Applications/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /Applications/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at KeymapManager.module.exports.KeymapManager.dispatchCommandEvent (/Applications/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:524:16)
  at KeymapManager.module.exports.KeymapManager.handleKeyboardEvent (/Applications/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:347:22)
  at HTMLDocument.module.exports.WindowEventHandler.onKeydown (/Applications/Atom.app/Contents/Resources/app.asar/src/window-event-handler.js:177:20)

Commands

     -0:58.1.0 core:backspace (atom-text-editor.editor.is-focused)
     -0:56.6.0 core:save (atom-text-editor.editor.is-focused)
     -0:38.3.0 editor:delete-to-beginning-of-line (atom-text-editor.editor.is-focused)
     -0:36.7.0 editor:select-line (atom-text-editor.editor.is-focused)
     -0:35.4.0 fuzzy-finder:toggle-file-finder (atom-text-editor.editor.is-focused)
     -0:34.6.0 editor:consolidate-selections (atom-text-editor.editor.mini.is-focused)
     -0:34.6.0 core:cancel (atom-text-editor.editor.mini.is-focused)
     -0:32.9.0 core:backspace (atom-text-editor.editor.is-focused)
     -0:32.7.0 editor:newline (atom-text-editor.editor.is-focused)
  2x -0:31.9.0 core:backspace (atom-text-editor.editor.is-focused)
     -0:31.5.0 core:move-up (atom-text-editor.editor.is-focused)
     -0:30.1.0 autocomplete-plus:confirm (atom-text-editor.editor.is-focused.autocomplete-active)
     -0:27.9.0 core:save (atom-text-editor.editor.is-focused)
  6x -0:05.5.0 core:move-left (atom-text-editor.editor.is-focused)
  5x -0:04.5.0 core:move-right (atom-text-editor.editor.is-focused)
     -0:00.9.0 language-idris:type-of (atom-text-editor.editor.is-focused)

Config

{
  "core": {
    "themes": [
      "one-light-ui",
      "one-light-syntax"
    ]
  },
  "language-idris": {
    "pathToIdris": "/Users/hannes/Library/Haskell/bin/idris"
  }
}

Installed Packages

# User
language-idris, v0.2.3

# Dev
No dev packages

Metavariables should maybe save the file or the new variables wont be shown

@david-christiansen how do you handle this in the emacs-mode? The ide-mode needs a saved file to analyze it. When I edit a file and then show the metavarables they will still be the same ones as last time you saved the file. Is it okay for me to just overwrite the file for the user?

I hope the question is clear :)

Program not loaded before running interactive editing commands

If I run the Add Clause command, I need to manually save the file before I can case split the resulting pattern variables, because otherwise, Idris hasn't re-typechecked.

In the Emacs mode, we check to see if the file has been modified since the last time it was type checked, and then invoke the type checker prior to running interactive editing commands. It might be good to do the same in Atom.

Syntax definition

As you have this point in the TODO list:

Improve the syntax-highlighting (the current is base on the Sublime plugin)

I suggest to collaborate on it. I've made some progress here (see yaml file), but I'm not very good in defining textmate scopes and there are some not defined things yet (see TODO comment at the bottom). So if you are interested, take it to your atom plugin and welcome to suggest improvements.

Fix parser for the ide-mode commands

the parser cannot handle escaped quotes in strings at the moment.
this means it cant parse this: (:return (:ok "\"Z\" : String" ((0 3 ((:name "\"Z\""))))) 5)

see failing test:
ac9d0b2

importing modules from the same directory in idris mode for atom fails

Reported by davidwlewis on IRC:

(00:18:44) davidwlewis: I'm having trouble importing modules from the same directory in idris mode for atom
(00:19:44) davidwlewis: I even hacked the way atom spawns the ide-mode process to add the project directory with the -i flag, no joy
(00:36:55) davidwlewis: Is this a limitation of ide-mode or is something busted at my end?
(00:55:34) christiansen` is now known as christiansen
(01:01:57) christiansen: davidwlewis: my guess is that the atom mode isn't setting the right working directory baed on the ipkg file
(01:02:04) christiansen: this is worth an issue there

Save before command isn't working properly.

I'm on v2.3.
Case splitting on one argument and then on another overrides the previous change - the command seems to work on the previous state of the text file.

Video:
http://screencast.com/t/2DW8pYMjBb

Abominably slow startup time.

This package adds 143ms to my startup time, compared to a typical 2ms-3ms for languages and 10ms for linters. Not cool.

Uncaught TypeError: Cannot read property 'stdin' of null

Install the package
Create a new buffer
Try to get docs with Ctrl-Opt-d or via the command palette

Atom Version: 1.0.5
System: Mac OS X 10.10.4
Thrown From: language-idris package, v0.2.1

Stack Trace

Uncaught TypeError: Cannot read property 'stdin' of null

At /Users/jeremy/.atom/packages/language-idris/lib/idris-ide-mode.coffee:24

TypeError: Cannot read property 'stdin' of null
  at IdrisIdeMode.send (/Users/jeremy/.atom/packages/language-idris/lib/idris-ide-mode.coffee:24:13)
  at IdrisModel.prepareCommand (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:58:16)
  at IdrisModel.docsFor (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:65:6)
  at IdrisController.getDocsForWord (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:79:8)
  at /Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at atom-text-editor.<anonymous> (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:48:9)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at KeymapManager.module.exports.KeymapManager.dispatchCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:524:16)
  at KeymapManager.module.exports.KeymapManager.handleKeyboardEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:347:22)
  at HTMLDocument.module.exports.WindowEventHandler.onKeydown (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/window-event-handler.js:177:20)

Commands

     -2:36.6.0 command-palette:toggle (atom-text-editor.editor.is-focused)
  7x -2:32.5.0 core:move-down (atom-text-editor.editor.mini.is-focused)
  3x -2:27.8.0 core:move-up (atom-text-editor.editor.mini.is-focused)
  7x -2:25.9.0 core:move-down (atom-text-editor.editor.mini.is-focused)
  9x -2:22.9.0 core:move-up (atom-text-editor.editor.mini.is-focused)
  3x -2:20.9.0 core:move-down (atom-text-editor.editor.mini.is-focused)
  3x -2:19.3.0 core:move-up (atom-text-editor.editor.mini.is-focused)
     -2:17.4.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -2:17.4.0 language-idris:docs-for (atom-text-editor.editor)
     -1:51.7.0 settings-view:open (atom-text-editor.editor.is-focused)
     -1:26.8.0 core:confirm (atom-text-editor#language-idris.pathToIdris.editor.mini.is-focused)
     -0:35.4.0 core:move-up (atom-text-editor.editor.is-focused)
  3x -0:34.8.0 core:move-right (atom-text-editor.editor.is-focused)
     -0:20.5.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:14 core:confirm (atom-text-editor.editor.mini.is-focused)
  2x -0:14 language-idris:docs-for (atom-text-editor.editor)

Config

{
  "core": {
    "themes": [
      "atom-material-ui",
      "atom-material-syntax"
    ]
  },
  "language-idris": {
    "pathToIdris": "/usr/local/bin/idris"
  }
}

Installed Packages

# User
atom-material-syntax, v0.2.1
atom-material-ui, v0.5.13
autocomplete-haskell, v0.4.5
haskell-ghc-mod, v0.8.8
ide-haskell, v0.7.1
language-haskell, v1.3.0
language-idris, v0.2.1

# Dev
No dev packages

Uncaught TypeError: Cannot read property 'setStatusLoaded' of null

[Enter steps to reproduce below:]

I launched atom with atom bounds.idr
Ran the typechecker with ctrl+option+R.

Atom Version: 1.0.15
System: Mac OS X 10.10.5
Thrown From: language-idris package, v0.3.0

Stack Trace

Uncaught TypeError: Cannot read property 'setStatusLoaded' of null

At /Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:549

TypeError: Cannot read property 'setStatusLoaded' of null
    at AnonymousObserver._onNext (/Users/chris/.atom/packages/language-idris/lib/idris-controller.coffee:128:32)
    at AnonymousObserver.Rx.AnonymousObserver.AnonymousObserver.next (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1811:12)
    at AnonymousObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
    at AnonymousObserver.tryCatcher (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
    at AutoDetachObserverPrototype.next (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
    at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)
    at FilterObserver.onNext (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:4114:34)
    at FilterObserver.tryCatcher (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:537:29)
    at AutoDetachObserverPrototype.next (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:5421:51)
    at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (/Users/chris/.atom/packages/language-idris/node_modules/rx-lite/rx.lite.js:1743:35)

Commands

     -0:02.3.0 language-idris:typecheck (atom-text-editor.editor.is-focused)

Config

{
  "core": {
    "themes": [
      "atom-dark-ui",
      "monokai"
    ],
    "ignoredNames": [
      ".git",
      ".svn",
      ".DS_Store"
    ]
  },
  "language-idris": {}
}

Installed Packages

# User
asciidoc-preview, v0.6.0
language-asciidoc, v0.12.0
language-idris, v0.3.0
monokai, v0.18.0

# Dev
No dev packages

Initial clause is inserted in wrong place for functions with multiline type annotation.

If function has several lines of type annotation then generated initial clause for it should be inserted in the annotation's following line instead the middle of type annotation.

Now it is not.
For example:

addMatrix : Num numType => Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)

after use ctrl+alt+a:

addMatrix : Num numType => Vect rows (Vect cols numType)
addMatrix xs ys = ?addMatrix_rhs
                           -> Vect rows (Vect cols numType)
                           -> Vect rows (Vect cols numType)

Uncaught Error: write EPIPE

[Enter steps to reproduce below:]

Atom Version: 1.0.11
System: Microsoft Windows 10 Pro
Thrown From: language-idris package, v0.2.4

Stack Trace

Uncaught Error: write EPIPE

At events.js:141

Error: write EPIPE
    at exports._errnoException (util.js:734:11)
    at Socket._writeGeneric (net.js:668:26)
    at Socket._write (net.js:687:8)
    at doWrite (_stream_writable.js:295:12)
    at writeOrBuffer (_stream_writable.js:282:5)
    at Socket.Writable.write (_stream_writable.js:210:11)
    at Socket.write (net.js:612:40)
    at IdrisIdeMode.send (C:\Users\J\.atom\packages\language-idris\lib\idris-ide-mode.coffee:24:20)
    at IdrisModel.prepareCommand (C:\Users\J\.atom\packages\language-idris\lib\idris-model.coffee:64:16)
    at IdrisModel.load (C:\Users\J\.atom\packages\language-idris\lib\idris-model.coffee:68:6)

Commands

  2x -3:11.9.0 editor:newline (atom-text-editor.editor.is-focused)
  5x -2:44.1.0 core:backspace (atom-text-editor.editor.is-focused)
     -2:37.3.0 editor:newline (atom-text-editor.editor.is-focused)
     -1:35.7.0 editor:move-to-end-of-screen-line (atom-text-editor.editor.is-focused)
     -1:34 editor:newline (atom-text-editor.editor.is-focused)
     -1:09.3.0 language-idris:typecheck (atom-text-editor.editor.is-focused)
     -0:34.5.0 core:save (atom-text-editor.editor.is-focused)
     -0:03.2.0 language-idris:typecheck (atom-text-editor.editor.is-focused)

Config

{}

Installed Packages

# User
language-idris, v0.2.4

# Dev
No dev packages

Implement a UI for the `apropos` command.

Implement a UI for the apropos command.

Uncaught TypeError: undefined is not a function

[Enter steps to reproduce below:]

Upgraded from 0.166.0
Start atom

Atom Version: 0.176.0
System: linux 3.18.3-031803-lowlatency
Thrown From: language-idris package, v0.0.1

Stack Trace

Uncaught TypeError: undefined is not a function

At /home/luis/.atom/packages/language-idris/lib/idris-controller.js:116

TypeError: undefined is not a function
  at IdrisController.paneChanged (/home/luis/.atom/packages/language-idris/lib/idris-controller.js:116:20)
  at atom-workspace.handler (/usr/share/atom/resources/app/src/space-pen-extensions.js:110:34)
  at atom-workspace.jQuery.event.dispatch (/usr/share/atom/resources/app/node_modules/space-pen/vendor/jquery.js:4681:9)
  at atom-workspace.elemData.handle (/usr/share/atom/resources/app/node_modules/space-pen/vendor/jquery.js:4359:46)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/usr/share/atom/resources/app/src/command-registry.js:243:29)
  at CommandRegistry.handleCommandEvent (/usr/share/atom/resources/app/src/command-registry.js:3:61)
  at CommandRegistry.module.exports.CommandRegistry.dispatch (/usr/share/atom/resources/app/src/command-registry.js:156:19)
  at PaneContainerView.jQuery.fn.trigger (/usr/share/atom/resources/app/src/space-pen-extensions.js:64:23)
  at PaneContainerView.module.exports.PaneContainerView.onActivePaneItemChanged (/usr/share/atom/resources/app/src/pane-container-view.js:53:19)
  at /usr/share/atom/resources/app/src/pane-container-view.js:3:61
  at Emitter.module.exports.Emitter.emit (/usr/share/atom/resources/app/node_modules/event-kit/lib/emitter.js:82:11)
  at /usr/share/atom/resources/app/src/pane-container.js:347:34
  at Emitter.module.exports.Emitter.emit (/usr/share/atom/resources/app/node_modules/event-kit/lib/emitter.js:82:11)
  at Pane.module.exports.Pane.setActiveItem (/usr/share/atom/resources/app/src/pane.js:264:22)
  at Pane.module.exports.Pane.activateItem (/usr/share/atom/resources/app/src/pane.js:328:21)
  at tabs-tab.<anonymous> (/usr/share/atom/resources/app/node_modules/tabs/lib/tab-bar-view.js:184:24)
  at space-pen-ul.jQuery.event.dispatch (/usr/share/atom/resources/app/node_modules/jquery/dist/jquery.js:4430:9)
  at space-pen-ul.elemData.handle (/usr/share/atom/resources/app/node_modules/jquery/dist/jquery.js:4116:28)

Commands

     -0:32.2 pane:reopen-closed-item (atom-text-editor.editor)
     -0:04.8 deprecation-cop:view (atom-workspace.workspace.scrollbars-visible-always.theme-atom-dark-syntax.theme-atom-dark-ui)

Config

{
  "core": {}
}

Installed Packages

# User
atom-grails, v0.1.0
ide-haskell, v0.3.0
language-clojure, v0.10.0
language-elm, v0.4.1
language-groovy, v0.3.0
language-haskell, v1.0.0
language-idris, v0.0.1
language-lua, v0.9.0
language-purescript, v0.2.0
language-scheme, v1.3.0
react, v0.9.7

# Dev
No dev packages

/cc @atom/core

Add an entry for proving to the tutorial

Most commands throw exceptions on Windows 8.1

There are two kind of exceptions:

Raised when using language-idris:docs-for

Atom Version: 1.0.19
System: Microsoft Windows 8.1
Thrown From: language-idris package, v0.3.2

Stack Trace

Uncaught TypeError: Cannot read property 'stdin' of null

At C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:549

TypeError: Cannot read property 'stdin' of null
  at IdrisIdeMode.send (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-ide-mode.coffee:51:13)
  at IdrisModel.prepareCommand (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:73:32)
  at IdrisModel.docsFor (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:98:6)
  at IdrisController.getDocsForWord (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:105:8)
  at C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:1:1
  at AnonymousObserver._onNext (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:63:11)
  at AnonymousObserver.Rx.AnonymousObserver.AnonymousObserver.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1811:12)
  at AnonymousObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at AnonymousObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at InnerObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3092:90)
  at InnerObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at scheduleItem (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2566:16)
  at Scheduler.scheduleNow [as _schedule] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1173:50)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:957:19)
  at JustSink.run (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2571:36)
  at JustObservable.subscribeCore (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2556:19)
  at JustObservable.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at [object Object].setDisposable [as action] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1984:46)
  at [object Object].ScheduledItem.invokeCore (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:916:17)
  at [object Object].ScheduledItem.invoke (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:904:40)
  at runTrampoline (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1186:37)
  at tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at Scheduler.scheduleNow [as _schedule] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1197:45)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:957:19)
  at JustObservable.subscribe [as _subscribe] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1996:32)
  at JustObservable.Rx.Observable.observableProto.subscribe.observableProto.forEach (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1873:19)
  at MergeAllObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3060:37)
  at MergeAllObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at MapObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3862:19)
  at MapObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at AsyncSubject.Rx.AsyncSubject.addProperties.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5631:17)
  at AsyncSubject.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1763:14)
  at AutoDetachObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1763:14)
  at handler (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:4223:20)
  at FSReqWrap.oncomplete (fs.js:82:15)

Commands

  2x -2:36.6.0 language-idris:docs-for (atom-text-editor.editor.is-focused)
     -1:51.7.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -1:51.7.0 core:cancel (atom-text-editor.editor.is-focused)
     -1:50.4.0 language-idris:typecheck (atom-text-editor.editor.is-focused)
     -1:49.8.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -1:49.8.0 core:cancel (atom-text-editor.editor.is-focused)
     -1:45.1.0 language-idris:case-split (atom-text-editor.editor.is-focused)
     -1:43.2.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -1:43.2.0 core:cancel (atom-text-editor.editor.is-focused)
     -1:38.9.0 build:select-active-target (atom-text-editor.editor.is-focused)
     -1:37.2.0 editor:consolidate-selections (atom-text-editor.editor.mini.is-focused)
     -1:37.2.0 core:cancel (atom-text-editor.editor.mini.is-focused)
     -1:17.6.0 language-idris:proof-search (atom-text-editor.editor.is-focused)
     -1:09.5.0 language-idris:make-with (atom-text-editor.editor.is-focused)
     -1:03.8.0 language-idris:make-lemma (atom-text-editor.editor.is-focused)
     -0:03.6.0 language-idris:docs-for (atom-text-editor.editor.is-focused)

Config

{
  "core": {
    "themes": [
      "atom-dark-ui",
      "atom-dark-syntax"
    ]
  },
  "language-idris": {}
}

Installed Packages

# User
autocomplete-haskell, v0.5.1
autocomplete-python, v0.5.4
build, v0.47.0
haskell-ghc-mod, v0.9.12
ide-haskell, v0.7.2
language-haskell, v1.4.9
language-idris, v0.3.2
language-rust, v0.4.5
racer, v0.17.2

# Dev
No dev packages

Raised when using language-idris:typecheck (and other commands)

Atom Version: 1.0.19
System: Microsoft Windows 8.1
Thrown From: language-idris package, v0.3.2

Stack Trace

Uncaught TypeError: Cannot read property 'length' of undefined

At C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:549

TypeError: Cannot read property 'length' of undefined
  at IdrisIdeMode.start (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-ide-mode.coffee:18:32)
  at IdrisModel.ideMode (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:19:19)
  at IdrisModel.prepareCommand (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:73:6)
  at IdrisModel.interpret (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:113:6)
  at IdrisModel.changeDirectory (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:77:6)
  at IdrisModel.load (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-model.coffee:89:10)
  at IdrisController.doMakeLemma (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:241:8)
  at C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:1:1
  at AnonymousObserver._onNext (C:\Users\Adolfo\.atom\packages\language-idris\lib\idris-controller.coffee:63:11)
  at AnonymousObserver.Rx.AnonymousObserver.AnonymousObserver.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1811:12)
  at AnonymousObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at AnonymousObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at InnerObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3092:90)
  at InnerObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at scheduleItem (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2566:16)
  at Scheduler.scheduleNow [as _schedule] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1173:50)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:957:19)
  at JustSink.run (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2571:36)
  at JustObservable.subscribeCore (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:2556:19)
  at JustObservable.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at [object Object].setDisposable [as action] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1984:46)
  at [object Object].ScheduledItem.invokeCore (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:916:17)
  at [object Object].ScheduledItem.invoke (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:904:40)
  at runTrampoline (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1186:37)
  at tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at Scheduler.scheduleNow [as _schedule] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1197:45)
  at Scheduler.Rx.Scheduler.schedulerProto.scheduleWithState (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:957:19)
  at JustObservable.subscribe [as _subscribe] (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1996:32)
  at JustObservable.Rx.Observable.observableProto.subscribe.observableProto.forEach (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1873:19)
  at MergeAllObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3060:37)
  at MergeAllObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at MapObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:3862:19)
  at MapObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.next (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5421:51)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onNext (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1743:35)
  at AsyncSubject.Rx.AsyncSubject.addProperties.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5631:17)
  at AsyncSubject.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1763:14)
  at AutoDetachObserver.tryCatcher (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:537:29)
  at AutoDetachObserverPrototype.completed (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:5435:56)
  at AutoDetachObserver.Rx.internals.AbstractObserver.AbstractObserver.onCompleted (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:1763:14)
  at handler (C:\Users\Adolfo\.atom\packages\language-idris\node_modules\rx-lite\rx.lite.js:4223:20)
  at FSReqWrap.oncomplete (fs.js:82:15)

Commands

     -3:17.6.0 settings-view:check-for-package-updates (atom-workspace.workspace.scrollbars-visible-always.theme-atom-dark-syntax.theme-atom-dark-ui)
  2x -1:36.4.0 language-idris:docs-for (atom-text-editor.editor.is-focused)
     -0:51.5.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -0:51.5.0 core:cancel (atom-text-editor.editor.is-focused)
     -0:50.2.0 language-idris:typecheck (atom-text-editor.editor.is-focused)
     -0:49.6.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -0:49.6.0 core:cancel (atom-text-editor.editor.is-focused)
     -0:44.9.0 language-idris:case-split (atom-text-editor.editor.is-focused)
     -0:43 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -0:43 core:cancel (atom-text-editor.editor.is-focused)
     -0:38.7.0 build:select-active-target (atom-text-editor.editor.is-focused)
     -0:37 editor:consolidate-selections (atom-text-editor.editor.mini.is-focused)
     -0:37 core:cancel (atom-text-editor.editor.mini.is-focused)
     -0:17.4.0 language-idris:proof-search (atom-text-editor.editor.is-focused)
     -0:09.3.0 language-idris:make-with (atom-text-editor.editor.is-focused)
     -0:03.6.0 language-idris:make-lemma (atom-text-editor.editor.is-focused)

Config

{
  "core": {
    "themes": [
      "atom-dark-ui",
      "atom-dark-syntax"
    ]
  },
  "language-idris": {}
}

Installed Packages

# User
autocomplete-haskell, v0.5.1
autocomplete-python, v0.5.4
build, v0.47.0
haskell-ghc-mod, v0.9.12
ide-haskell, v0.7.2
language-haskell, v1.4.9
language-idris, v0.3.2
language-rust, v0.4.5
racer, v0.17.2

# Dev
No dev packages

The Idris Errors panel should tell me if typechecking went successfully

If I do typecheck and it fails, it raises the Idris Errors panel.
If I fix everything, typecheck again and it succeeds, currently there is no response what-so-ever and the old type error is still present.
I think there should be some indication that typechecking succeeded, and the old type error should not be displayed anymore.

Save before executing idris commands

I suppose this is a design decision.
Currently, it queries idris with the last saved version of the file.

I don't see where this would be preferred over querying over the current content that's visible on the screen.
Therefore, I believe that there should be an automatic save before executing commands.

Uncaught Error: This socket has been ended by the other party

I'm not finding any crash report for the idris executable.

Enter this code (I'm working on the "Well-Typed Interpreter" example):

import Data.Vect

-- Start by representing our universe as a product type.
data Ty = TyInt | TyBool | TyFun Ty Ty

interpret : Ty -> Type
interpret TyInt = Int
interpret TyBool = Bool
interpret (TyFun A T) = interpret A -> interpret T

-- G represents our expression environment.
let Env = Vect n Ty
using (G: Env)
    data Expr : Env -> Ty -> Type

Try to typecheck it. You'll see a "process crashed" message about the idris process exiting with code 1.
Try to typecheck it again. This and each further attempt gives this error about writing to a socket whose other end is closed. This error seems to recur each time I try to typecheck.

I have no idea how to try to restart the connection short of relaunching the entire editor. Suggestions:

Add a "relaunch idris" command
Relaunch and reconnect to it automatically (at least a couple times, to avoid spinning on repeated crashers) when it's detected as having exited, since much of the package functionality relies on it

Atom Version: 1.0.5
System: Mac OS X 10.10.4
Thrown From: language-idris package, v0.2.4

Stack Trace

Uncaught Error: This socket has been ended by the other party

At events.js:141

Error: This socket has been ended by the other party
  at Socket.writeAfterFIN [as write] (net.js:275:12)
  at IdrisIdeMode.send (/Users/jeremy/.atom/packages/language-idris/lib/idris-ide-mode.coffee:24:20)
  at IdrisModel.prepareCommand (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:64:16)
  at IdrisModel.load (/Users/jeremy/.atom/packages/language-idris/lib/idris-model.coffee:68:6)
  at IdrisController.typecheckFile (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:70:8)
  at /Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:1:1
  at atom-text-editor.<anonymous> (/Users/jeremy/.atom/packages/language-idris/lib/idris-controller.coffee:51:7)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at CommandPaletteView.module.exports.CommandPaletteView.confirmed (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/command-palette/lib/command-palette-view.js:159:32)
  at CommandPaletteView.module.exports.SelectListView.confirmSelection (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:338:21)
  at space-pen-div.atom.commands.add.core:confirm (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-space-pen-views/lib/select-list-view.js:109:19)
  at CommandRegistry.module.exports.CommandRegistry.handleCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:241:29)
  at /opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/command-registry.js:3:61
  at KeymapManager.module.exports.KeymapManager.dispatchCommandEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:524:16)
  at KeymapManager.module.exports.KeymapManager.handleKeyboardEvent (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/node_modules/atom-keymap/lib/keymap-manager.js:347:22)
  at HTMLDocument.module.exports.WindowEventHandler.onKeydown (/opt/homebrew-cask/Caskroom/atom/1.0.5/Atom.app/Contents/Resources/app.asar/src/window-event-handler.js:177:20)

Commands

     -0:47.6.0 core:move-right (atom-text-editor.editor.is-focused)
  3x -0:47.4.0 editor:select-to-beginning-of-word (atom-text-editor.editor.is-focused)
     -0:45.9.0 core:save (atom-text-editor.editor.is-focused.autocomplete-active)
     -0:45.7.0 core:move-down (atom-text-editor.editor.is-focused)
  4x -0:45.4.0 editor:move-to-end-of-word (atom-text-editor.editor.is-focused)
  3x -0:44.2.0 editor:select-to-beginning-of-word (atom-text-editor.editor.is-focused)
     -0:42.7.0 core:save (atom-text-editor.editor.is-focused.autocomplete-active)
     -0:25 editor:move-to-end-of-screen-line (atom-text-editor.editor.is-focused)
     -0:23.1.0 core:save (atom-text-editor.editor.is-focused)
  2x -0:15 language-idris:typecheck (atom-text-editor.editor.is-focused)
     -0:08.5.0 editor:consolidate-selections (atom-text-editor.editor.is-focused)
     -0:08.5.0 core:cancel (atom-text-editor.editor.is-focused)
     -0:06.1.0 command-palette:toggle (atom-text-editor.editor.is-focused)
     -0:04.7.0 core:backspace (atom-text-editor.editor.mini.is-focused)
     -0:01.1.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:01.1.0 language-idris:typecheck (atom-text-editor.editor)

Config

{
  "core": {
    "themes": [
      "atom-material-ui",
      "atom-material-syntax"
    ]
  },
  "language-idris": {
    "pathToIdris": "/usr/local/bin/idris"
  }
}

Installed Packages

# User
atom-material-syntax, v0.2.2
atom-material-ui, v0.5.13
autocomplete-haskell, v0.4.5
haskell-ghc-mod, v0.8.9
ide-haskell, v0.7.1
language-haskell, v1.3.1
language-idris, v0.2.4

# Dev
No dev packages

Uncaught TypeError: undefined is not a function

[Enter steps to reproduce below:]

installed language-idris plugin

Atom Version: 0.204.0
System: Mac OS X 10.10.3
Thrown From: language-idris package, v0.1.1

Stack Trace

Uncaught TypeError: undefined is not a function

At /Users/bob/.atom/packages/language-idris/lib/idris-controller.coffee:29

TypeError: undefined is not a function
  at new IdrisController (/Users/bob/.atom/packages/language-idris/lib/idris-controller.coffee:29:21)
  at Socket.module.exports.startIdrisProcesses (/Users/bob/.atom/packages/language-idris/lib/language-idris.coffee:35:11)
  at emitOne (events.js:82:20)
  at Socket.emit (events.js:166:7)
  at readableAddChunk (_stream_readable.js:146:16)
  at Socket.Readable.push (_stream_readable.js:109:10)
  at Pipe.onread (net.js:517:20)

Commands

     -0:35.8.0 command-palette:toggle (atom-pane.pane.active)
  5x -0:33.6.0 core:move-down (atom-text-editor.editor.mini.is-focused)
     -0:31.6.0 core:confirm (atom-text-editor.editor.mini.is-focused)
     -0:31.6.0 settings-view:install-packages-and-themes (atom-pane.pane.active)
  2x -0:24.9.0 core:confirm (atom-text-editor.editor.mini.is-focused)

Config

{
  "core": {
    "themes": [
      "atom-dark-ui",
      "atom-dark-syntax"
    ]
  }
}

Installed Packages

# User
autocomplete-elixir, v1.2.6
haskell-ghc-mod, v0.6.3
ide-haskell, v0.5.7
iex, v0.9.9
language-elixir, v0.5.0
language-haskell, v1.0.0
language-idris, v0.1.1
linter, v0.12.6
linter-elixirc, v0.2.2
vim-mode, v0.49.0

# Dev
No dev packages

IPKG: uses wrong folder when no sourcedir option was specified

it should start the compiler from the same directory as the file if no sourcedir option was specified in the ipkg file (or there is no ipkg file)

Add a means of setting the Idris -p option

Idris has a global library installation directory which is divided into packages. The prelude and base packages are always available for import, but further packages need to be enabled by passing Idris the -p PKGNAME command-line option.

This is something that's project-specific, so it doesn't really make sense in the global Idris configuration area (though that can be a temporary stopgap).

In the Emacs mode, we set this option in two ways:

We check if the user has set an Emacs file variable to a list of packages, and use them if so. File variables allow an Emacs Lisp variable to have a particular value when editing a particular file, and the value is stored in a specially-formatted comment. I'm not sure if Atom has a similar feature or not.
If the file being edited is in a directory that contains a .ipkg file, or a subdirectory of such a directory, that file is processed to find the list of packages that a command-line invocation of idris would get from the package commands (e.g. --build, --install). These are then passed to the Idris subprocess.

I don't know the right solution for Atom, but it's pretty important to be able to do this.

Error when searching for type, documentation

plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r
plusAssoc Z c r = Refl
plusAssoc (S l) c r = rewrite plusAssoc l c r in Refl

select Nat and do a typesearch.

The package will send Nat) to Idris, resulting in the type not being found.

Cannot get documentation or types for operators

The operators are being sent as they appear in the code, but they need parenthesis around them.

:: -> (::)

Ensure that keybindings only work on Idris files

from your todo list:

When Atom supports it, ensure that they only work in the grammar scopes that they should work in.

take a look at atom-keymap-plus, I use this in my plugins to make sure my commands only triggers in the specified files 😉

as you can see here all my packages have the same keybinding but only one is triggered based on the file type

Add proof mode

see https://www.youtube.com/watch?v=0eOY1NxbZHo&list=PLiHLLF-foEexGJu1a0WH_llkQ2gOKqipg

Better error reporting

As reported by @edwinb in https://youtu.be/X36ye-1x_HQ?t=32m33s

The error messages look like this currently:

They can't be styled and they don't have any syntax highlighting

Add Semantic Highlighting to the TextEditor

ide-mode gives us back data on how to highlight the sourcecode:
http://docs.idris-lang.org/en/latest/reference/ide-protocol.html#source-code-highlighting

this would need some sort of dynamic grammar

see discussions on how to do it:
https://discuss.atom.io/t/syntax-highlighting-using-existing-tokenizer/13608
https://discuss.atom.io/t/automatically-update-to-dynamic-grammar/10181
https://discuss.atom.io/t/defining-a-language-grammar-via-code/14784/2
https://discuss.atom.io/t/dynamic-grammers/14927/3

Release v.0.1.0

I'd like to realease the next version.

@Heather do you know of any bugs?
@morten do you want to remain official author of this package?
https://github.com/idris-hackers/atom-language-idris/blob/master/package.json#L13

idris-hackers / atom-language-idris Goto Github PK

atom-language-idris's People

Contributors

Stargazers

Watchers

Forkers

atom-language-idris's Issues

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Raised when using language-idris:docs-for

Stack Trace

Commands

Config

Installed Packages

Raised when using language-idris:typecheck (and other commands)

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Stack Trace

Commands

Config

Installed Packages

Recommend Projects

Recommend Topics

Recommend Org