From c98aabdf019caea7e38e8d7b4298c1ce61b4bcbb Mon Sep 17 00:00:00 2001
From: Markus Klink <markus.klink@inoio.de>
Date: Tue, 4 Sep 2018 14:02:03 +0200
Subject: [PATCH] Prevent idris compiler crash when sending wrong make-with
 command

---
 lib/idris-controller.coffee | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

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 <tt>' + word + '</tt> ...'
 
     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 }) =>