1.1 --- a/src/Pure/PIDE/document.scala	Sun Feb 26 16:02:53 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Sun Feb 26 16:17:57 2012 +0100
     1.3 @@ -191,10 +191,13 @@
     1.4  
     1.5    object Change
     1.6    {
     1.7 -    val init: Change = Change()
     1.8 +    val init: Change = new Change()
     1.9 +
    1.10 +    def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
    1.11 +      new Change(Some(previous), edits, version)
    1.12    }
    1.13  
    1.14 -  sealed case class Change(
    1.15 +  class Change private(
    1.16      val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
    1.17      val edits: List[Edit_Text] = Nil,
    1.18      val version: Future[Version] = Future.value(Version.init))
    1.19 @@ -203,7 +206,7 @@
    1.20        (previous match { case None => true case Some(future) => future.is_finished }) &&
    1.21        version.is_finished
    1.22  
    1.23 -    def truncate: Change = copy(previous = None, edits = Nil)
    1.24 +    def truncate: Change = new Change(None, Nil, version)
    1.25    }
    1.26  
    1.27  
    1.28 @@ -391,7 +394,7 @@
    1.29          edits: List[Edit_Text],
    1.30          version: Future[Version]): (Change, State) =
    1.31      {
    1.32 -      val change = Change(Some(previous), edits, version)
    1.33 +      val change = Change.make(previous, edits, version)
    1.34        (change, copy(history = history + change))
    1.35      }
    1.36