Robust real-time synchronization between textual and graphical editors