src/Pure/System/session.scala
changeset 38425 e467db701d78
parent 38424 940a404e45e2
child 38446 9d59dab38fef
--- a/src/Pure/System/session.scala	Sun Aug 15 21:03:13 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 15 21:42:13 2010 +0200
@@ -292,7 +292,7 @@
   {
     @volatile private var history = Document.History.init
 
-    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
       history.snapshot(name, pending_edits, current_state())
 
     def act
@@ -328,7 +328,7 @@
 
   def stop() { session_actor ! Stop }
 
-  def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
+  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
     editor_history.snapshot(name, pending_edits)
 
   def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }