src/Pure/PIDE/document.scala
changeset 49346 977cf0788b30
parent 48923 a2df77fcf1eb
child 49414 d7b5fb2e9ca2
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Sep 13 11:13:00 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Sep 13 16:01:42 2012 +0200
     1.3 @@ -290,6 +290,7 @@
     1.4      def convert(range: Text.Range): Text.Range
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range
     1.7 +    def eq_markup(other: Snapshot): Boolean
     1.8      def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
     1.9        result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
    1.10      def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.11 @@ -479,7 +480,8 @@
    1.12  
    1.13  
    1.14      // persistent user-view
    1.15 -    def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
    1.16 +    def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
    1.17 +      : Snapshot =
    1.18      {
    1.19        val stable = recent_stable
    1.20        val latest = history.tip
    1.21 @@ -503,6 +505,16 @@
    1.22          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.23          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.24  
    1.25 +        def eq_markup(other: Snapshot): Boolean =
    1.26 +          !is_outdated && !other.is_outdated &&
    1.27 +            node.commands.size == other.node.commands.size &&
    1.28 +            ((node.commands.iterator zip other.node.commands.iterator) forall {
    1.29 +              case (cmd1, cmd2) =>
    1.30 +                cmd1.source == cmd2.source &&
    1.31 +                (state.command_state(version, cmd1).markup eq
    1.32 +                 other.state.command_state(other.version, cmd2).markup)
    1.33 +            })
    1.34 +
    1.35          def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.36            result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.37          {