# HG changeset patch
# User wenzelm
# Date 1364051446 -3600
# Node ID 8f3d1a7bee261621f3e046bef491286a2b42dff1
# Parent  59d8a1031c00a409b7338a22beba6c708475494c
structural equality for Command.Results;
more general Command.State.eq_content;

diff -r 59d8a1031c00 -r 8f3d1a7bee26 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Mar 23 13:57:46 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Mar 23 16:10:46 2013 +0100
@@ -25,7 +25,7 @@
     def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
   }
 
-  final class Results private(rep: SortedMap[Long, XML.Tree])
+  final class Results private(private val rep: SortedMap[Long, XML.Tree])
   {
     def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
     def get(serial: Long): Option[XML.Tree] = rep.get(serial)
@@ -40,6 +40,12 @@
       else if (rep.isEmpty) other
       else (this /: other.entries)(_ + _)
 
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Results => rep == other.rep
+        case _ => false
+      }
     override def toString: String = entries.mkString("Results(", ", ", ")")
   }
 
@@ -56,7 +62,13 @@
       markup.to_XML(command.range, command.source, filter)
 
 
-    /* accumulate content */
+    /* content */
+
+    def eq_content(other: State): Boolean =
+      command.source == other.command.source &&
+      status == other.status &&
+      results == other.results &&
+      markup == other.markup
 
     private def add_status(st: Markup): State = copy(status = st :: status)
     private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
diff -r 59d8a1031c00 -r 8f3d1a7bee26 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Mar 23 13:57:46 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Mar 23 16:10:46 2013 +0100
@@ -277,7 +277,7 @@
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
-    def eq_markup(other: Snapshot): Boolean
+    def eq_content(other: Snapshot): Boolean
     def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
       result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range, elements: Option[Set[String]],
@@ -494,14 +494,13 @@
         def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
         def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
 
-        def eq_markup(other: Snapshot): Boolean =
+        def eq_content(other: Snapshot): Boolean =
           !is_outdated && !other.is_outdated &&
             node.commands.size == other.node.commands.size &&
             ((node.commands.iterator zip other.node.commands.iterator) forall {
               case (cmd1, cmd2) =>
-                cmd1.source == cmd2.source &&
-                (state.command_state(version, cmd1).markup eq
-                 other.state.command_state(other.version, cmd2).markup)
+                state.command_state(version, cmd1) eq_content
+                  other.state.command_state(other.version, cmd2)
             })
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
diff -r 59d8a1031c00 -r 8f3d1a7bee26 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Sat Mar 23 13:57:46 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Sat Mar 23 16:10:46 2013 +0100
@@ -101,7 +101,7 @@
 
           if (!(line_count == last_line_count && char_count == last_char_count &&
                 L == last_L && H == last_H && relevant_range == last_relevant_range &&
-                (snapshot eq_markup last_snapshot) && (options eq last_options)))
+                (snapshot eq_content last_snapshot) && (options eq last_options)))
           {
             @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
               : List[(Color, Int, Int)] =