From db0f62a2d91f40c245943becfe5a5effdc60f6a6 Mon Sep 17 00:00:00 2001 From: Markus Klink Date: Thu, 6 Sep 2018 17:21:38 +0200 Subject: [PATCH] Fixes #206 --- lib/idris-controller.coffee | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index be68a7e..51248ce 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -327,7 +327,7 @@ class IdrisController .filter ({ responseType }) -> responseType == 'return' .flatMap => @model.makeWith line + 1, word .subscribe successHandler, @displayErrors - else + else @clearMessagePanel "Idris: Illegal position to make a with view" # construct a lemma from a hole @@ -402,6 +402,7 @@ class IdrisController editor.transact -> # Delete old line, insert the new case block + editor.moveToBeginningOfLine() editor.deleteLine() editor.insertText clause # And move the cursor to the beginning of