Merge pull request #162 from zjhmale/save-editor

Save editor before executing commands
idris-hackers · Apr 8, 2017 · 6a8fff5 · 6a8fff5
2 parents 4dade4a + f041cde
commit 6a8fff5
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)