src/Pure/System/session.scala
changeset 38260 d4a1c7a19be3
parent 38230 ed147003de4b
child 38355 8cb265fb12fe
     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  }