src/Pure/System/session.scala
changeset 38365 7c6254a9c432
parent 38364 827b90f18ff4
child 38366 fea82d1add74
     1.1 --- a/src/Pure/System/session.scala	Thu Aug 12 16:01:44 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 16:23:04 2010 +0200
     1.3 @@ -320,7 +320,27 @@
     1.4    private val editor_history = new Actor
     1.5    {
     1.6      @volatile private var history = Document.Change.init
     1.7 -    def current_change(): Document.Change = history
     1.8 +
     1.9 +    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
    1.10 +    {
    1.11 +      val latest = history
    1.12 +      val stable = latest.ancestors.find(_.is_assigned)
    1.13 +      require(stable.isDefined)
    1.14 +
    1.15 +      val edits =
    1.16 +        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
    1.17 +            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
    1.18 +      lazy val reverse_edits = edits.reverse
    1.19 +
    1.20 +      new Document.Snapshot {
    1.21 +        val document = stable.get.join_document
    1.22 +        val node = document.nodes(name)
    1.23 +        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
    1.24 +        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    1.25 +        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.26 +        def state(command: Command): Command.State = document.current_state(command)
    1.27 +      }
    1.28 +    }
    1.29  
    1.30      def act
    1.31      {
    1.32 @@ -356,7 +376,7 @@
    1.33    def stop() { session_actor ! Stop }
    1.34  
    1.35    def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
    1.36 -    editor_history.current_change().snapshot(name, pending_edits)
    1.37 +    editor_history.snapshot(name, pending_edits)
    1.38  
    1.39    def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
    1.40  }