simplified/clarified Change: transition prev --edits--> result, based on futures;
authorwenzelm
Thu Aug 12 17:37:58 2010 +0200 (2010-08-12)
changeset 38366fea82d1add74
parent 38365 7c6254a9c432
child 38367 f7d2574dc3a6
simplified/clarified Change: transition prev --edits--> result, based on futures;
Session.history: plain List instead of somewhat indirect Change.ancestors;
tuned;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 12 16:23:04 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 12 17:37:58 2010 +0200
     1.3 @@ -107,27 +107,17 @@
     1.4  
     1.5    object Change
     1.6    {
     1.7 -    val init = new Change(None, Nil, Future.value(Nil, Document.init))
     1.8 +    val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
     1.9    }
    1.10  
    1.11    class Change(
    1.12 -    val parent: Option[Change],
    1.13 +    val prev: Future[Document],
    1.14      val edits: List[Node_Text_Edit],
    1.15      val result: Future[(List[Edit[Command]], Document)])
    1.16    {
    1.17 -    def ancestors: Iterator[Change] = new Iterator[Change]
    1.18 -    {
    1.19 -      private var state: Option[Change] = Some(Change.this)
    1.20 -      def hasNext = state.isDefined
    1.21 -      def next =
    1.22 -        state match {
    1.23 -          case Some(change) => state = change.parent; change
    1.24 -          case None => throw new NoSuchElementException("next on empty iterator")
    1.25 -        }
    1.26 -    }
    1.27 -
    1.28 -    def join_document: Document = result.join._2
    1.29 -    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.30 +    val document: Future[Document] = result.map(_._2)
    1.31 +    def is_finished: Boolean = prev.is_finished && document.is_finished
    1.32 +    def is_assigned: Boolean = is_finished && document.join.assignment.is_finished
    1.33    }
    1.34  
    1.35  
     2.1 --- a/src/Pure/System/session.scala	Thu Aug 12 16:23:04 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Thu Aug 12 17:37:58 2010 +0200
     2.3 @@ -99,9 +99,11 @@
     2.4      def handle_change(change: Document.Change)
     2.5      //{{{
     2.6      {
     2.7 -      require(change.parent.isDefined)
     2.8 +      require(change.is_finished)
     2.9  
    2.10 +      val old_id = change.prev.join.id
    2.11        val (node_edits, doc) = change.result.join
    2.12 +
    2.13        val id_edits =
    2.14          node_edits map {
    2.15            case (name, None) => (name, None)
    2.16 @@ -125,7 +127,7 @@
    2.17              (name -> Some(chs))
    2.18          }
    2.19        register_document(doc)
    2.20 -      prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits)
    2.21 +      prover.edit_document(old_id, doc.id, id_edits)
    2.22      }
    2.23      //}}}
    2.24  
    2.25 @@ -319,23 +321,25 @@
    2.26  
    2.27    private val editor_history = new Actor
    2.28    {
    2.29 -    @volatile private var history = Document.Change.init
    2.30 +    @volatile private var history = List(Document.Change.init)
    2.31  
    2.32      def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
    2.33      {
    2.34 -      val latest = history
    2.35 -      val stable = latest.ancestors.find(_.is_assigned)
    2.36 -      require(stable.isDefined)
    2.37 +      val history_snapshot = history
    2.38 +
    2.39 +      require(history_snapshot.exists(_.is_assigned))
    2.40 +      val latest = history_snapshot.head
    2.41 +      val stable = history_snapshot.find(_.is_assigned).get
    2.42  
    2.43        val edits =
    2.44 -        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
    2.45 +        (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
    2.46              (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
    2.47        lazy val reverse_edits = edits.reverse
    2.48  
    2.49        new Document.Snapshot {
    2.50 -        val document = stable.get.join_document
    2.51 +        val document = stable.document.join
    2.52          val node = document.nodes(name)
    2.53 -        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
    2.54 +        val is_outdated = !(pending_edits.isEmpty && latest == stable)
    2.55          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
    2.56          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    2.57          def state(command: Command): Command.State = document.current_state(command)
    2.58 @@ -347,16 +351,19 @@
    2.59        loop {
    2.60          react {
    2.61            case Edit_Document(edits) =>
    2.62 -            val old_change = history
    2.63 +            val history_snapshot = history
    2.64 +            require(!history_snapshot.isEmpty)
    2.65 +
    2.66 +            val prev = history_snapshot.head.document
    2.67              val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
    2.68                isabelle.Future.fork {
    2.69 -                val old_doc = old_change.join_document
    2.70 +                val old_doc = prev.join
    2.71                  old_doc.await_assignment
    2.72                  Document.text_edits(Session.this, old_doc, edits)
    2.73                }
    2.74 -            val new_change = new Document.Change(Some(old_change), edits, result)
    2.75 -            history = new_change
    2.76 -            new_change.result.map(_ => session_actor ! new_change)
    2.77 +            val new_change = new Document.Change(prev, edits, result)
    2.78 +            history ::= new_change
    2.79 +            new_change.document.map(_ => session_actor ! new_change)
    2.80              reply(())
    2.81  
    2.82            case bad => System.err.println("editor_model: ignoring bad message " + bad)