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