more careful treatment of multiple command states (eval + prints): merge content that is actually required;
authorwenzelm
Thu Mar 27 10:43:43 2014 +0100 (2014-03-27)
changeset 562998201790fdeb9
parent 56298 cf7710540f39
child 56300 8346b664fa7a
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/query_operation.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Mar 26 21:01:09 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Mar 27 10:43:43 2014 +0100
     1.3 @@ -27,8 +27,8 @@
     1.4    {
     1.5      type Entry = (Long, XML.Tree)
     1.6      val empty = new Results(SortedMap.empty)
     1.7 -    def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
     1.8 -    def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
     1.9 +    def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
    1.10 +    def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
    1.11    }
    1.12  
    1.13    final class Results private(private val rep: SortedMap[Long, XML.Tree])
    1.14 @@ -98,6 +98,15 @@
    1.15  
    1.16    /* state */
    1.17  
    1.18 +  object State
    1.19 +  {
    1.20 +    def merge_results(states: List[State]): Command.Results =
    1.21 +      Results.merge(states.map(_.results))
    1.22 +
    1.23 +    def merge_markup(states: List[State], index: Markup_Index): Markup_Tree =
    1.24 +      Markup_Tree.merge(states.map(_.markup(index)))
    1.25 +  }
    1.26 +
    1.27    sealed case class State(
    1.28      command: Command,
    1.29      status: List[Markup] = Nil,
    1.30 @@ -108,9 +117,6 @@
    1.31  
    1.32      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.33  
    1.34 -    def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
    1.35 -      markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
    1.36 -
    1.37  
    1.38      /* content */
    1.39  
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Mar 26 21:01:09 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 27 10:43:43 2014 +0100
     2.3 @@ -630,25 +630,35 @@
     2.4          assignments = assignments1)
     2.5      }
     2.6  
     2.7 -    def command_state(version: Version, command: Command): Command.State =
     2.8 +    def command_states(version: Version, command: Command): List[Command.State] =
     2.9      {
    2.10        require(is_assigned(version))
    2.11        try {
    2.12          the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
    2.13            .map(the_dynamic_state(_)) match {
    2.14 -            case eval_state :: print_states => (eval_state /: print_states)(_ ++ _)
    2.15              case Nil => fail
    2.16 +            case states => states
    2.17            }
    2.18        }
    2.19        catch {
    2.20          case _: State.Fail =>
    2.21 -          try { the_static_state(command.id) }
    2.22 -          catch { case _: State.Fail => command.init_state }
    2.23 +          try { List(the_static_state(command.id)) }
    2.24 +          catch { case _: State.Fail => List(command.init_state) }
    2.25        }
    2.26      }
    2.27  
    2.28 +    def command_results(version: Version, command: Command): Command.Results =
    2.29 +      Command.State.merge_results(command_states(version, command))
    2.30 +
    2.31 +    def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
    2.32 +      Command.State.merge_markup(command_states(version, command), index)
    2.33 +
    2.34      def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body =
    2.35 -      node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten
    2.36 +      (for {
    2.37 +        command <- node.commands.iterator
    2.38 +        markup = command_markup(version, command, Command.Markup_Index.markup)
    2.39 +        tree <- markup.to_XML(command.range, command.source, filter)
    2.40 +      } yield tree).toList
    2.41  
    2.42      // persistent user-view
    2.43      def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil)
    2.44 @@ -691,8 +701,12 @@
    2.45          def eq_content(other: Snapshot): Boolean =
    2.46          {
    2.47            def eq_commands(commands: (Command, Command)): Boolean =
    2.48 -            state.command_state(version, commands._1) eq_content
    2.49 -              other.state.command_state(other.version, commands._2)
    2.50 +          {
    2.51 +            val states1 = state.command_states(version, commands._1)
    2.52 +            val states2 = other.state.command_states(other.version, commands._2)
    2.53 +            states1.length == states2.length &&
    2.54 +            (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 })
    2.55 +          }
    2.56  
    2.57            !is_outdated && !other.is_outdated &&
    2.58            node.commands.size == other.node.commands.size &&
    2.59 @@ -718,9 +732,9 @@
    2.60                val markup_index = Command.Markup_Index(status, file_name)
    2.61                (for {
    2.62                  chunk <- thy_load_command.chunks.get(file_name).iterator
    2.63 -                st = state.command_state(version, thy_load_command)
    2.64 -                res = result(st.results)
    2.65 -                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    2.66 +                states = state.command_states(version, thy_load_command)
    2.67 +                res = result(Command.State.merge_results(states))
    2.68 +                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    2.69                    former_range.restrict(chunk.range), info, elements,
    2.70                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    2.71                  ).iterator
    2.72 @@ -730,9 +744,9 @@
    2.73                val markup_index = Command.Markup_Index(status, "")
    2.74                (for {
    2.75                  (command, command_start) <- node.command_range(former_range)
    2.76 -                st = state.command_state(version, command)
    2.77 -                res = result(st.results)
    2.78 -                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
    2.79 +                states = state.command_states(version, command)
    2.80 +                res = result(Command.State.merge_results(states))
    2.81 +                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    2.82                    (former_range - command_start).restrict(command.range), info, elements,
    2.83                    {
    2.84                      case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
     3.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Mar 26 21:01:09 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 10:43:43 2014 +0100
     3.3 @@ -20,6 +20,9 @@
     3.4  
     3.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
     3.6  
     3.7 +  def merge(trees: List[Markup_Tree]): Markup_Tree =
     3.8 +    (empty /: trees)(_ ++ _)
     3.9 +
    3.10    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    3.11      trees match {
    3.12        case Nil => empty
    3.13 @@ -157,8 +160,12 @@
    3.14    }
    3.15  
    3.16    def ++ (other: Markup_Tree): Markup_Tree =
    3.17 -    (this /: other.branches)({ case (tree, (range, entry)) =>
    3.18 -      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
    3.19 +    if (this eq other) this
    3.20 +    else if (branches.isEmpty) other
    3.21 +    else
    3.22 +      (this /: other.branches)({ case (tree, (range, entry)) =>
    3.23 +        ((tree ++ entry.subtree) /: entry.markup)(
    3.24 +          { case (t, elem) => t + Text.Info(range, elem) }) })
    3.25  
    3.26    def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
    3.27    {
     4.1 --- a/src/Pure/PIDE/protocol.scala	Wed Mar 26 21:01:09 2014 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 27 10:43:43 2014 +0100
     4.3 @@ -117,18 +117,19 @@
     4.4      var finished = 0
     4.5      var warned = 0
     4.6      var failed = 0
     4.7 -    node.commands.foreach(command =>
     4.8 -      {
     4.9 -        val st = state.command_state(version, command)
    4.10 -        val status = command_status(st.status)
    4.11 -        if (status.is_running) running += 1
    4.12 -        else if (status.is_finished) {
    4.13 -          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
    4.14 -          else finished += 1
    4.15 -        }
    4.16 -        else if (status.is_failed) failed += 1
    4.17 -        else unprocessed += 1
    4.18 -      })
    4.19 +    for {
    4.20 +      command <- node.commands
    4.21 +      st <- state.command_states(version, command)
    4.22 +      status = command_status(st.status)
    4.23 +    } {
    4.24 +      if (status.is_running) running += 1
    4.25 +      else if (status.is_finished) {
    4.26 +        if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
    4.27 +        else finished += 1
    4.28 +      }
    4.29 +      else if (status.is_failed) failed += 1
    4.30 +      else unprocessed += 1
    4.31 +    }
    4.32      Node_Status(unprocessed, running, finished, warned, failed)
    4.33    }
    4.34  
    4.35 @@ -149,7 +150,7 @@
    4.36      var commands = Map.empty[Command, Double]
    4.37      for {
    4.38        command <- node.commands.iterator
    4.39 -      st = state.command_state(version, command)
    4.40 +      st <- state.command_states(version, command)
    4.41        command_timing =
    4.42          (0.0 /: st.status)({
    4.43            case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
     5.1 --- a/src/Pure/PIDE/query_operation.scala	Wed Mar 26 21:01:09 2014 +0100
     5.2 +++ b/src/Pure/PIDE/query_operation.scala	Thu Mar 27 10:43:43 2014 +0100
     5.3 @@ -70,20 +70,20 @@
     5.4  
     5.5      /* snapshot */
     5.6  
     5.7 -    val (snapshot, state, removed) =
     5.8 +    val (snapshot, command_results, removed) =
     5.9        current_location match {
    5.10          case Some(cmd) =>
    5.11            val snapshot = editor.node_snapshot(cmd.node_name)
    5.12 -          val state = snapshot.state.command_state(snapshot.version, cmd)
    5.13 +          val command_results = snapshot.state.command_results(snapshot.version, cmd)
    5.14            val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd)
    5.15 -          (snapshot, state, removed)
    5.16 +          (snapshot, command_results, removed)
    5.17          case None =>
    5.18 -          (Document.Snapshot.init, Command.empty.init_state, true)
    5.19 +          (Document.Snapshot.init, Command.Results.empty, true)
    5.20        }
    5.21  
    5.22      val results =
    5.23        (for {
    5.24 -        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries
    5.25 +        (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries
    5.26          if props.contains((Markup.INSTANCE, instance))
    5.27        } yield elem).toList
    5.28  
    5.29 @@ -154,7 +154,7 @@
    5.30          current_update_pending = false
    5.31          if (current_output != new_output && !removed) {
    5.32            current_output = new_output
    5.33 -          consume_output(snapshot, state.results, new_output)
    5.34 +          consume_output(snapshot, command_results, new_output)
    5.35          }
    5.36          if (current_status != new_status) {
    5.37            current_status = new_status
     6.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Mar 26 21:01:09 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 27 10:43:43 2014 +0100
     6.3 @@ -160,8 +160,7 @@
     6.4          val root = data.root
     6.5          for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     6.6            val markup =
     6.7 -            snapshot.state.command_state(snapshot.version, command).
     6.8 -              markup(Command.Markup_Index.markup)
     6.9 +            snapshot.state.command_markup(snapshot.version, command, Command.Markup_Index.markup)
    6.10            Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
    6.11                {
    6.12                  val range = info.range + command_start
     7.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Mar 26 21:01:09 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Mar 27 10:43:43 2014 +0100
     7.3 @@ -27,7 +27,8 @@
     7.4    private var zoom_factor = 100
     7.5    private var do_update = true
     7.6    private var current_snapshot = Document.Snapshot.init
     7.7 -  private var current_state = Command.empty.init_state
     7.8 +  private var current_command = Command.empty
     7.9 +  private var current_results = Command.Results.empty
    7.10    private var current_output: List[XML.Tree] = Nil
    7.11  
    7.12  
    7.13 @@ -49,33 +50,34 @@
    7.14    {
    7.15      Swing_Thread.require()
    7.16  
    7.17 -    val (new_snapshot, new_state) =
    7.18 +    val (new_snapshot, new_command, new_results) =
    7.19        PIDE.editor.current_node_snapshot(view) match {
    7.20          case Some(snapshot) =>
    7.21            if (follow && !snapshot.is_outdated) {
    7.22              PIDE.editor.current_command(view, snapshot) match {
    7.23                case Some(cmd) =>
    7.24 -                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    7.25 +                (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
    7.26                case None =>
    7.27 -                (Document.Snapshot.init, Command.empty.init_state)
    7.28 +                (Document.Snapshot.init, Command.empty, Command.Results.empty)
    7.29              }
    7.30            }
    7.31 -          else (current_snapshot, current_state)
    7.32 -        case None => (current_snapshot, current_state)
    7.33 +          else (current_snapshot, current_command, current_results)
    7.34 +        case None => (current_snapshot, current_command, current_results)
    7.35        }
    7.36  
    7.37      val new_output =
    7.38 -      if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
    7.39 +      if (!restriction.isDefined || restriction.get.contains(new_command)) {
    7.40          val rendering = Rendering(new_snapshot, PIDE.options.value)
    7.41 -        rendering.output_messages(new_state)
    7.42 +        rendering.output_messages(new_results)
    7.43        }
    7.44        else current_output
    7.45  
    7.46      if (new_output != current_output)
    7.47 -      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
    7.48 +      pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
    7.49  
    7.50      current_snapshot = new_snapshot
    7.51 -    current_state = new_state
    7.52 +    current_command = new_command
    7.53 +    current_results = new_results
    7.54      current_output = new_output
    7.55    }
    7.56  
    7.57 @@ -149,8 +151,7 @@
    7.58      tooltip = "Detach window with static copy of current output"
    7.59      reactions += {
    7.60        case ButtonClicked(_) =>
    7.61 -        Info_Dockable(view, current_snapshot,
    7.62 -          current_state.results, Pretty.separate(current_output))
    7.63 +        Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output))
    7.64      }
    7.65    }
    7.66  
     8.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 26 21:01:09 2014 +0100
     8.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Mar 27 10:43:43 2014 +0100
     8.3 @@ -592,8 +592,8 @@
     8.4      message_colors.get(pri).map((_, is_separator))
     8.5    }
     8.6  
     8.7 -  def output_messages(st: Command.State): List[XML.Tree] =
     8.8 -    st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
     8.9 +  def output_messages(results: Command.Results): List[XML.Tree] =
    8.10 +    results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
    8.11  
    8.12  
    8.13    /* text background */
     9.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Wed Mar 26 21:01:09 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Thu Mar 27 10:43:43 2014 +0100
     9.3 @@ -26,7 +26,8 @@
     9.4    /* component state -- owned by Swing thread */
     9.5  
     9.6    private var current_snapshot = Document.State.init.snapshot()
     9.7 -  private var current_state = Command.empty.init_state
     9.8 +  private var current_command = Command.empty
     9.9 +  private var current_results = Command.Results.empty
    9.10    private var current_id = 0L
    9.11    private var do_update = true
    9.12    private var do_auto_reply = false
    9.13 @@ -77,7 +78,7 @@
    9.14  
    9.15    private def show_trace()
    9.16    {
    9.17 -    val trace = Simplifier_Trace.generate_trace(current_state.results)
    9.18 +    val trace = Simplifier_Trace.generate_trace(current_results)
    9.19      new Simplifier_Trace_Window(view, current_snapshot, trace)
    9.20    }
    9.21  
    9.22 @@ -92,7 +93,7 @@
    9.23    {
    9.24      set_context(
    9.25        current_snapshot,
    9.26 -      Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results)
    9.27 +      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
    9.28      )
    9.29    }
    9.30  
    9.31 @@ -103,23 +104,24 @@
    9.32  
    9.33    private def handle_update(follow: Boolean)
    9.34    {
    9.35 -    val (new_snapshot, new_state, new_id) =
    9.36 +    val (new_snapshot, new_command, new_results, new_id) =
    9.37        PIDE.editor.current_node_snapshot(view) match {
    9.38          case Some(snapshot) =>
    9.39            if (follow && !snapshot.is_outdated) {
    9.40              PIDE.editor.current_command(view, snapshot) match {
    9.41                case Some(cmd) =>
    9.42 -                (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id)
    9.43 +                (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
    9.44                case None =>
    9.45 -                (Document.State.init.snapshot(), Command.empty.init_state, 0L)
    9.46 +                (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
    9.47              }
    9.48            }
    9.49 -          else (current_snapshot, current_state, current_id)
    9.50 -        case None => (current_snapshot, current_state, current_id)
    9.51 +          else (current_snapshot, current_command, current_results, current_id)
    9.52 +        case None => (current_snapshot, current_command, current_results, current_id)
    9.53        }
    9.54  
    9.55      current_snapshot = new_snapshot
    9.56 -    current_state = new_state
    9.57 +    current_command = new_command
    9.58 +    current_results = new_results
    9.59      current_id = new_id
    9.60      update_contents()
    9.61    }