edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;

--- 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) }
 }