diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index 9551749..be68a7e 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -189,6 +189,7 @@ class IdrisController @saveFile editor uri = editor.getURI() word = Symbol.serializeWord editorHelper.getWordUnderCursor(editor) + @clearMessagePanel 'Idris: Searching type of ' + word + ' ...' successHandler = ({ responseType, msg }) => @@ -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 }) =>