src/Pure/PIDE/document.scala
changeset 56299 8201790fdeb9
parent 56298 cf7710540f39
child 56300 8346b664fa7a
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 21:01:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 27 10:43:43 2014 +0100
     1.3 @@ -630,25 +630,35 @@
     1.4          assignments = assignments1)
     1.5      }
     1.6  
     1.7 -    def command_state(version: Version, command: Command): Command.State =
     1.8 +    def command_states(version: Version, command: Command): List[Command.State] =
     1.9      {
    1.10        require(is_assigned(version))
    1.11        try {
    1.12          the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
    1.13            .map(the_dynamic_state(_)) match {
    1.14 -            case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
    1.15              case Nil => fail
    1.16 +            case states => states
    1.17            }
    1.18        }
    1.19        catch {
    1.20          case _: State.Fail =>
    1.21 -          try { the_static_state(command.id) }
    1.22 -          catch { case _: State.Fail => command.init_state }
    1.23 +          try { List(the_static_state(command.id)) }
    1.24 +          catch { case _: State.Fail => List(command.init_state) }
    1.25        }
    1.26      }
    1.27  
    1.28 +    def command_results(version: Version, command: Command): Command.Results =
    1.29 +      Command.State.merge_results(command_states(version, command))
    1.30 +
    1.31 +    def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
    1.32 +      Command.State.merge_markup(command_states(version, command), index)
    1.33 +
    1.34      def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
    1.35 -      node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten
    1.36 +      (for {
    1.37 +        command <- node.commands.iterator
    1.38 +        markup = command_markup(version, command, Command.Markup_Index.markup)
    1.39 +        tree <- markup.to_XML(command.range, command.source, filter)
    1.40 +      } yield tree).toList
    1.41  
    1.42      // persistent user-view
    1.43      def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
    1.44 @@ -691,8 +701,12 @@
    1.45          def eq_content(other: Snapshot): Boolean =
    1.46          {
    1.47            def eq_commands(commands: (Command, Command)): Boolean =
    1.48 -            state.command_state(version, commands._1) eq_content
    1.49 -              other.state.command_state(other.version, commands._2)
    1.50 +          {
    1.51 +            val states1 = state.command_states(version, commands._1)
    1.52 +            val states2 = other.state.command_states(other.version, commands._2)
    1.53 +            states1.length == states2.length &&
    1.54 +            (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 })
    1.55 +          }
    1.56  
    1.57            !is_outdated && !other.is_outdated &&
    1.58            node.commands.size == other.node.commands.size &&
    1.59 @@ -718,9 +732,9 @@
    1.60                val markup_index = Command.Markup_Index(status, file_name)
    1.61                (for {
    1.62                  chunk <- thy_load_command.chunks.get(file_name).iterator
    1.63 -                st = state.command_state(version, thy_load_command)
    1.64 -                res = result(st.results)
    1.65 -                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.66 +                states = state.command_states(version, thy_load_command)
    1.67 +                res = result(Command.State.merge_results(states))
    1.68 +                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    1.69                    former_range.restrict(chunk.range), info, elements,
    1.70                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    1.71                  ).iterator
    1.72 @@ -730,9 +744,9 @@
    1.73                val markup_index = Command.Markup_Index(status, "")
    1.74                (for {
    1.75                  (command, command_start) <- node.command_range(former_range)
    1.76 -                st = state.command_state(version, command)
    1.77 -                res = result(st.results)
    1.78 -                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    1.79 +                states = state.command_states(version, command)
    1.80 +                res = result(Command.State.merge_results(states))
    1.81 +                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    1.82                    (former_range - command_start).restrict(command.range), info, elements,
    1.83                    {
    1.84                      case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))