scala-ide/scala-ide — pull request #857 by sschaef (2014-11-10 21:45:00+00:00)
Title: Update editor only once after execution of save actions

Updating the editor is expensive, therefore we only want to do it a
single time - at the end of the save action running phase.

Fixes #1002309