more explicit treatment of cleared nodes (removal is implicit);
authorwenzelm
Wed Jul 23 16:20:07 2014 +0200 (2014-07-23)
changeset 57620c30ab960875e
parent 57619 dcd69422b953
child 57621 caa37976801f
more explicit treatment of cleared nodes (removal is implicit);
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 15:32:05 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 16:20:07 2014 +0200
     1.3 @@ -363,12 +363,12 @@
     1.4      val init: Change = new Change()
     1.5  
     1.6      def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change =
     1.7 -      new Change(Some(previous), edits, version)
     1.8 +      new Change(Some(previous), edits.reverse, version)
     1.9    }
    1.10  
    1.11    final class Change private(
    1.12      val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
    1.13 -    val edits: List[Edit_Text] = Nil,
    1.14 +    val rev_edits: List[Edit_Text] = Nil,
    1.15      val version: Future[Version] = Future.value(Version.init))
    1.16    {
    1.17      def is_finished: Boolean =
    1.18 @@ -717,10 +717,24 @@
    1.19        val stable = recent_stable
    1.20        val latest = history.tip
    1.21  
    1.22 -      // FIXME proper treatment of removed nodes
    1.23 +
    1.24 +      /* pending edits and unstable changes */
    1.25 +
    1.26 +      val rev_pending_changes =
    1.27 +        for {
    1.28 +          change <- history.undo_list.takeWhile(_ != stable)
    1.29 +          (a, edits) <- change.rev_edits
    1.30 +          if a == name
    1.31 +        } yield edits
    1.32 +
    1.33 +      val is_cleared = rev_pending_changes.exists({ case Node.Clear() => true case _ => false })
    1.34        val edits =
    1.35 -        (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
    1.36 -            (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits)
    1.37 +        if (is_cleared) Nil
    1.38 +        else
    1.39 +          (pending_edits /: rev_pending_changes)({
    1.40 +            case (edits, Node.Edits(es)) => es ::: edits
    1.41 +            case (edits, _) => edits
    1.42 +          })
    1.43        lazy val reverse_edits = edits.reverse
    1.44  
    1.45        new Snapshot
    1.46 @@ -734,10 +748,13 @@
    1.47  
    1.48          /* local node content */
    1.49  
    1.50 -        def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
    1.51 -        def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.52 -        def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.53 -        def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.54 +        def convert(offset: Text.Offset) =
    1.55 +          if (is_cleared) 0 else (offset /: edits)((i, edit) => edit.convert(i))
    1.56 +        def revert(offset: Text.Offset) =
    1.57 +          if (is_cleared) 0 else (offset /: reverse_edits)((i, edit) => edit.revert(i))
    1.58 +
    1.59 +        def convert(range: Text.Range) = range.map(convert(_))
    1.60 +        def revert(range: Text.Range) = range.map(revert(_))
    1.61  
    1.62          val node_name = name
    1.63          val node = version.nodes(name)
     2.1 --- a/src/Pure/PIDE/text.scala	Wed Jul 23 15:32:05 2014 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Wed Jul 23 16:20:07 2014 +0200
     2.3 @@ -154,8 +154,6 @@
     2.4  
     2.5      def convert(i: Offset): Offset = transform(is_insert, i)
     2.6      def revert(i: Offset): Offset = transform(!is_insert, i)
     2.7 -    def convert(range: Range): Range = range.map(convert)
     2.8 -    def revert(range: Range): Range = range.map(revert)
     2.9  
    2.10  
    2.11      /* edit strings */