# HG changeset patch
# User wenzelm
# Date 1281622984 -7200
# Node ID 7c6254a9c432d7ee5b3c96ddc709b00a2cbdf1f7
# Parent  827b90f18ff424b340816b3d5ab58d03603b4a55
moved snapshot to Session (cf. 96b22dfeb56a);

diff -r 827b90f18ff4 -r 7c6254a9c432 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 12 16:01:44 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 12 16:23:04 2010 +0200
@@ -128,27 +128,6 @@
 
     def join_document: Document = result.join._2
     def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
-
-    def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
-    {
-      val latest = Change.this
-      val stable = latest.ancestors.find(_.is_assigned)
-      require(stable.isDefined)
-
-      val edits =
-        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
-            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
-      lazy val reverse_edits = edits.reverse
-
-      new Snapshot {
-        val document = stable.get.join_document
-        val node = document.nodes(name)
-        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
-        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
-        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
-        def state(command: Command): Command.State = document.current_state(command)
-      }
-    }
   }
 
 
diff -r 827b90f18ff4 -r 7c6254a9c432 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Aug 12 16:01:44 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 12 16:23:04 2010 +0200
@@ -320,7 +320,27 @@
   private val editor_history = new Actor
   {
     @volatile private var history = Document.Change.init
-    def current_change(): Document.Change = history
+
+    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+    {
+      val latest = history
+      val stable = latest.ancestors.find(_.is_assigned)
+      require(stable.isDefined)
+
+      val edits =
+        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
+            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+      lazy val reverse_edits = edits.reverse
+
+      new Document.Snapshot {
+        val document = stable.get.join_document
+        val node = document.nodes(name)
+        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
+        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
+        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+        def state(command: Command): Command.State = document.current_state(command)
+      }
+    }
 
     def act
     {
@@ -356,7 +376,7 @@
   def stop() { session_actor ! Stop }
 
   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
-    editor_history.current_change().snapshot(name, pending_edits)
+    editor_history.snapshot(name, pending_edits)
 
   def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
 }