src/Pure/PIDE/document.scala
changeset 44436 546adfa8a6fc
parent 44385 e7fdb008aa7d
child 44442 cb18e4f09053
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 23 21:19:24 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Aug 24 13:03:39 2011 +0200
     1.3 @@ -146,7 +146,8 @@
     1.4      val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
     1.5    }
     1.6  
     1.7 -  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
     1.8 +  type Nodes = Map[String, Node]
     1.9 +  sealed case class Version(val id: Version_ID, val nodes: Nodes)
    1.10  
    1.11  
    1.12    /* changes of plain text, eventually resulting in document edits */
    1.13 @@ -290,6 +291,12 @@
    1.14          case None => false
    1.15        }
    1.16  
    1.17 +    def is_stable(change: Change): Boolean =
    1.18 +      change.is_finished && is_assigned(change.version.get_finished)
    1.19 +
    1.20 +    def tip_stable: Boolean = is_stable(history.tip)
    1.21 +    def recent_stable: Option[Change] = history.undo_list.find(is_stable)
    1.22 +
    1.23      def extend_history(previous: Future[Version],
    1.24          edits: List[Edit_Text],
    1.25          version: Future[Version]): (Change, State) =
    1.26 @@ -302,11 +309,8 @@
    1.27      // persistent user-view
    1.28      def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    1.29      {
    1.30 -      val found_stable = history.undo_list.find(change =>
    1.31 -        change.is_finished && is_assigned(change.version.get_finished))
    1.32 -      require(found_stable.isDefined)
    1.33 -      val stable = found_stable.get
    1.34 -      val latest = history.undo_list.head
    1.35 +      val stable = recent_stable.get
    1.36 +      val latest = history.tip
    1.37  
    1.38        // FIXME proper treatment of removed nodes
    1.39        val edits =