# HG changeset patch
# User wenzelm
# Date 1330269477 -3600
# Node ID c2dba08548f9d46c4d1961c6f79cf50399c42d17
# Parent  388ba4daae05948df94b029c2859aa121bfc612d
more abstract class Document.Change;

diff -r 388ba4daae05 -r c2dba08548f9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 26 16:02:53 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 16:17:57 2012 +0100
@@ -191,10 +191,13 @@
 
   object Change
   {
-    val init: Change = Change()
+    val init: Change = new Change()
+
+    def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
+      new Change(Some(previous), edits, version)
   }
 
-  sealed case class Change(
+  class Change private(
     val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
     val edits: List[Edit_Text] = Nil,
     val version: Future[Version] = Future.value(Version.init))
@@ -203,7 +206,7 @@
       (previous match { case None => true case Some(future) => future.is_finished }) &&
       version.is_finished
 
-    def truncate: Change = copy(previous = None, edits = Nil)
+    def truncate: Change = new Change(None, Nil, version)
   }
 
 
@@ -391,7 +394,7 @@
         edits: List[Edit_Text],
         version: Future[Version]): (Change, State) =
     {
-      val change = Change(Some(previous), edits, version)
+      val change = Change.make(previous, edits, version)
       (change, copy(history = history + change))
     }