1.1 --- a/src/Pure/System/session.scala	Thu Aug 12 13:42:05 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 13:43:55 2010 +0200
     1.3 @@ -356,7 +356,8 @@
     1.4  
     1.5    def stop() { session_actor ! Stop }
     1.6  
     1.7 -  def current_change(): Document.Change = editor_history.current_change()
     1.8 +  def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
     1.9 +    editor_history.current_change().snapshot(name, pending_edits)
    1.10  
    1.11    def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
    1.12  }

     2.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 12 13:42:05 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 12 13:43:55 2010 +0200
     2.3 @@ -227,7 +227,7 @@
     2.4  
     2.5    def snapshot(): Document.Snapshot = {
     2.6      Swing_Thread.require()
     2.7 -    session.current_change().snapshot(thy_name, pending_edits.snapshot())
     2.8 +    session.snapshot(thy_name, pending_edits.snapshot())
     2.9    }
    2.10  
    2.11