You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
The text was updated successfully, but these errors were encountered:
consumeStatusBar: (statusBar) ->
atom.workspace.onDidChangeActivePaneItem (paneItem) ->
console.log("active pane item is:", paneItem)
/* (jws/2015-08-28)TODO: add/remove status based on if it is/not an Idris file */
@controller.attachStatusIndicator statusBar
It logs whenever I switch tabs. Should be able to spelunk into the provided object to work out if it's an Idris file or not. The best way to go is likely based on the grammar rather than the file extension, since if the grammar is not set to idris, then none of our functions will be available anyway (right?).
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:The text was updated successfully, but these errors were encountered: