# HG changeset patch
# User wenzelm
# Date 1281613435 -7200
# Node ID 96b22dfeb56a20cee664051db1bb2ddd38d7bdb1
# Parent  15819cbd7b0e1a71378579e01eefb5fc6d90870e
consider snapshot as service of Session, not Document.Change;

diff -r 15819cbd7b0e -r 96b22dfeb56a src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Aug 12 13:42:05 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 12 13:43:55 2010 +0200
@@ -356,7 +356,8 @@
 
   def stop() { session_actor ! Stop }
 
-  def current_change(): Document.Change = editor_history.current_change()
+  def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+    editor_history.current_change().snapshot(name, pending_edits)
 
   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
 }
diff -r 15819cbd7b0e -r 96b22dfeb56a src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 12 13:42:05 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 12 13:43:55 2010 +0200
@@ -227,7 +227,7 @@
 
   def snapshot(): Document.Snapshot = {
     Swing_Thread.require()
-    session.current_change().snapshot(thy_name, pending_edits.snapshot())
+    session.snapshot(thy_name, pending_edits.snapshot())
   }