# HG changeset patch
# User wenzelm
# Date 1281442550 -7200
# Node ID d4a1c7a19be3dd7c9109d87934f837cba4709ecc
# Parent  2b61c5e27399612875bd3c69c798f5dd6d239b19
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;

diff -r 2b61c5e27399 -r d4a1c7a19be3 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 10 12:29:11 2010 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 10 14:15:50 2010 +0200
@@ -334,6 +334,7 @@
             val new_change = new Document.Change(new_id, Some(old_change), edits, result)
             history = new_change
             new_change.result.map(_ => session_actor ! new_change)
+            reply(())
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)
         }
@@ -352,5 +353,6 @@
   def stop() { session_actor ! Stop }
 
   def current_change(): Document.Change = editor_history.current_change()
-  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
+
+  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
 }