--- 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))
}