more accurate eq_content;
authorwenzelm
Wed Feb 12 11:05:48 2014 +0100 (2014-02-12)
changeset 55434aa2918d967f0
parent 55433 d2960d67f163
child 55435 662e0fd39823
more accurate eq_content;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Feb 12 10:50:49 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Feb 12 11:05:48 2014 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4        command.source == other.command.source &&
     1.5        status == other.status &&
     1.6        results == other.results &&
     1.7 -      markup == other.markup
     1.8 +      markups == other.markups
     1.9  
    1.10      private def add_status(st: Markup): State = copy(status = st :: status)
    1.11  
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Feb 12 10:50:49 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Feb 12 11:05:48 2014 +0100
     2.3 @@ -614,13 +614,17 @@
     2.4            else version.nodes.thy_load_commands(node_name)
     2.5  
     2.6          def eq_content(other: Snapshot): Boolean =
     2.7 +        {
     2.8 +          def eq_commands(commands: (Command, Command)): Boolean =
     2.9 +            state.command_state(version, commands._1) eq_content
    2.10 +              other.state.command_state(other.version, commands._2)
    2.11 +
    2.12            !is_outdated && !other.is_outdated &&
    2.13 -            node.commands.size == other.node.commands.size &&
    2.14 -            ((node.commands.iterator zip other.node.commands.iterator) forall {
    2.15 -              case (cmd1, cmd2) =>
    2.16 -                state.command_state(version, cmd1) eq_content
    2.17 -                  other.state.command_state(other.version, cmd2)
    2.18 -            })
    2.19 +          node.commands.size == other.node.commands.size &&
    2.20 +          (node.commands.iterator zip other.node.commands.iterator).forall(eq_commands) &&
    2.21 +          thy_load_commands.length == other.thy_load_commands.length &&
    2.22 +          (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
    2.23 +        }
    2.24  
    2.25          def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    2.26            result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =