# HG changeset patch
# User wenzelm
# Date 1392199548 -3600
# Node ID aa2918d967f07ef524bf89b682864844d03270f4
# Parent  d2960d67f163ac1ca6eee853714574ad76b3333d
more accurate eq_content;

diff -r d2960d67f163 -r aa2918d967f0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Feb 12 10:50:49 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Feb 12 11:05:48 2014 +0100
@@ -77,7 +77,7 @@
       command.source == other.command.source &&
       status == other.status &&
       results == other.results &&
-      markup == other.markup
+      markups == other.markups
 
     private def add_status(st: Markup): State = copy(status = st :: status)
 
diff -r d2960d67f163 -r aa2918d967f0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Feb 12 10:50:49 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Feb 12 11:05:48 2014 +0100
@@ -614,13 +614,17 @@
           else version.nodes.thy_load_commands(node_name)
 
         def eq_content(other: Snapshot): Boolean =
+        {
+          def eq_commands(commands: (Command, Command)): Boolean =
+            state.command_state(version, commands._1) eq_content
+              other.state.command_state(other.version, commands._2)
+
           !is_outdated && !other.is_outdated &&
-            node.commands.size == other.node.commands.size &&
-            ((node.commands.iterator zip other.node.commands.iterator) forall {
-              case (cmd1, cmd2) =>
-                state.command_state(version, cmd1) eq_content
-                  other.state.command_state(other.version, cmd2)
-            })
+          node.commands.size == other.node.commands.size &&
+          (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
+          thy_load_commands.length == other.thy_load_commands.length &&
+          (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
+        }
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
           result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =