Save editor before executing commands

idris-hackers · Apr 5, 2017 · f041cde · f041cde
1 parent 4dade4a
commit f041cde
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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)