edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
authorwenzelm
Tue Aug 10 14:15:50 2010 +0200 (2010-08-10)
changeset 38260d4a1c7a19be3
parent 38259 2b61c5e27399
child 38261 4863a3816fc1
edit_document: synchronous reply to ensure consistent state wrt. calling (AWT) thread;
src/Pure/System/session.scala
     1.1 --- a/src/Pure/System/session.scala	Tue Aug 10 12:29:11 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Tue Aug 10 14:15:50 2010 +0200
     1.3 @@ -334,6 +334,7 @@
     1.4              val new_change = new Document.Change(new_id, Some(old_change), edits, result)
     1.5              history = new_change
     1.6              new_change.result.map(_ => session_actor ! new_change)
     1.7 +            reply(())
     1.8  
     1.9            case bad => System.err.println("editor_model: ignoring bad message " + bad)
    1.10          }
    1.11 @@ -352,5 +353,6 @@
    1.12    def stop() { session_actor ! Stop }
    1.13  
    1.14    def current_change(): Document.Change = editor_history.current_change()
    1.15 -  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history ! Edit_Document(edits) }
    1.16 +
    1.17 +  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
    1.18  }