From f041cded490a798bce4d636e8a919f2eb30585d6 Mon Sep 17 00:00:00 2001 From: zjhmale Date: Wed, 5 Apr 2017 11:55:17 +0800 Subject: [PATCH] Save editor before executing commands --- lib/idris-controller.coffee | 2 ++ 1 file changed, 2 insertions(+) diff --git a/lib/idris-controller.coffee b/lib/idris-controller.coffee index cdc5209..83abaee 100644 --- a/lib/idris-controller.coffee +++ b/lib/idris-controller.coffee @@ -131,6 +131,7 @@ class IdrisController getDocsForWord: ({ target }) => editor = @getEditor() + @saveFile editor uri = editor.getURI() word = Symbol.serializeWord @getWordUnderCursor(editor) @@ -370,6 +371,7 @@ class IdrisController printDefinition: ({ target }) => editor = @getEditor() + @saveFile editor uri = editor.getURI() word = Symbol.serializeWord @getWordUnderCursor(editor)