Skip to content

Commit

Permalink
Prevent idris compiler crash when sending wrong make-with command
Browse files Browse the repository at this point in the history
  • Loading branch information
Markus Klink committed Sep 4, 2018
1 parent 7f015f8 commit c98aabd
Showing 1 changed file with 9 additions and 6 deletions.
15 changes: 9 additions & 6 deletions lib/idris-controller.coffee
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,7 @@ class IdrisController
@saveFile editor
uri = editor.getURI()
word = Symbol.serializeWord editorHelper.getWordUnderCursor(editor)

@clearMessagePanel 'Idris: Searching type of <tt>' + word + '</tt> ...'

successHandler = ({ responseType, msg }) =>
Expand Down Expand Up @@ -320,12 +321,14 @@ class IdrisController
editor.moveToBeginningOfLine()
editor.moveUp()


@model
.load uri
.filter ({ responseType }) -> responseType == 'return'
.flatMap => @model.makeWith line + 1, word
.subscribe successHandler, @displayErrors
if (word?.length)
@model
.load uri
.filter ({ responseType }) -> responseType == 'return'
.flatMap => @model.makeWith line + 1, word
.subscribe successHandler, @displayErrors
else
@clearMessagePanel "Idris: Illegal position to make a with view"

# construct a lemma from a hole
doMakeLemma: ({ target }) =>
Expand Down

0 comments on commit c98aabd

Please sign in to comment.