Skip to content

Commit

Permalink
Merge pull request #218 from justjoheinz/bug/196
Browse files Browse the repository at this point in the history
ESC will close information panel
  • Loading branch information
justjoheinz authored Sep 19, 2018
2 parents 8ae8c8e + 979c241 commit 3c10161
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 4 deletions.
6 changes: 4 additions & 2 deletions keymaps/language-idris.json
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,8 @@
"ctrl-alt-r": "language-idris:typecheck",
"ctrl-alt-m": "language-idris:make-case",
"ctrl-alt-p": "language-idris:add-proof-clause",
"ctrl-alt-b": "language-idris:browse-namespace"
"ctrl-alt-b": "language-idris:browse-namespace",
"escape": "language-idris:close-information-view"
},

".platform-darwin, atom-text-editor[data-grammar~=\"idris\"]": {
Expand All @@ -26,6 +27,7 @@
"ctrl-cmd-r": "language-idris:typecheck",
"ctrl-cmd-m": "language-idris:make-case",
"ctrl-cmd-p": "language-idris:add-proof-clause",
"ctrl-cmd-b": "language-idris:browse-namespace"
"ctrl-cmd-b": "language-idris:browse-namespace",
"escape": "language-idris:close-information-view"
}
}
5 changes: 3 additions & 2 deletions lib/idris-controller.coffee
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ class IdrisController
'language-idris:apropos': @runCommand @apropos
'language-idris:add-proof-clause': @runCommand @doAddProofClause
'language-idris:browse-namespace': @runCommand @doBrowseNamespace
'language-idris:close-information-view': @hideAndClearMessagePanel

isIdrisFile: (uri) ->
uri?.match? /\.idr$/
Expand Down Expand Up @@ -70,14 +71,14 @@ class IdrisController
@statusbar.destroy()

# clear the message panel and optionally display a new title
clearMessagePanel: (title) ->
clearMessagePanel: (title) =>
@messages.attach()
@messages.show()
@messages.clear()
@messages.setTitle title, true if title?

# hide the message panel
hideAndClearMessagePanel: () ->
hideAndClearMessagePanel: () =>
@clearMessagePanel()
@messages.hide()

Expand Down

0 comments on commit 3c10161

Please sign in to comment.