# HG changeset patch # User wenzelm # Date 1395913423 -3600 # Node ID 8201790fdeb93c2d4ccf728df1f0784cb10fe12a # Parent cf7710540f39afeae386ec5acaf32020669df3a4 more careful treatment of multiple command states (eval + prints): merge content that is actually required; more standard Markup_Tree merge, including trivial cases; diff -r cf7710540f39 -r 8201790fdeb9 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Pure/PIDE/command.scala Thu Mar 27 10:43:43 2014 +0100 @@ -27,8 +27,8 @@ { type Entry = (Long, XML.Tree) val empty = new Results(SortedMap.empty) - def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _) - def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _) + def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _) + def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Tree]) @@ -98,6 +98,15 @@ /* state */ + object State + { + def merge_results(states: List[State]): Command.Results = + Results.merge(states.map(_.results)) + + def merge_markup(states: List[State], index: Markup_Index): Markup_Tree = + Markup_Tree.merge(states.map(_.markup(index))) + } + sealed case class State( command: Command, status: List[Markup] = Nil, @@ -108,9 +117,6 @@ def markup(index: Markup_Index): Markup_Tree = markups(index) - def markup_to_XML(filter: XML.Elem => Boolean): XML.Body = - markup(Markup_Index.markup).to_XML(command.range, command.source, filter) - /* content */ diff -r cf7710540f39 -r 8201790fdeb9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Pure/PIDE/document.scala Thu Mar 27 10:43:43 2014 +0100 @@ -630,25 +630,35 @@ assignments = assignments1) } - def command_state(version: Version, command: Command): Command.State = + def command_states(version: Version, command: Command): List[Command.State] = { require(is_assigned(version)) try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) .map(the_dynamic_state(_)) match { - case eval_state :: print_states => (eval_state /: print_states)(_ ++ _) case Nil => fail + case states => states } } catch { case _: State.Fail => - try { the_static_state(command.id) } - catch { case _: State.Fail => command.init_state } + try { List(the_static_state(command.id)) } + catch { case _: State.Fail => List(command.init_state) } } } + def command_results(version: Version, command: Command): Command.Results = + Command.State.merge_results(command_states(version, command)) + + def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree = + Command.State.merge_markup(command_states(version, command), index) + def markup_to_XML(version: Version, node: Node, filter: XML.Elem => Boolean): XML.Body = - node.commands.toList.map(cmd => command_state(version, cmd).markup_to_XML(filter)).flatten + (for { + command <- node.commands.iterator + markup = command_markup(version, command, Command.Markup_Index.markup) + tree <- markup.to_XML(command.range, command.source, filter) + } yield tree).toList // persistent user-view def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) @@ -691,8 +701,12 @@ 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) + { + val states1 = state.command_states(version, commands._1) + val states2 = other.state.command_states(other.version, commands._2) + states1.length == states2.length && + (states1 zip states2).forall({ case (st1, st2) => st1 eq_content st2 }) + } !is_outdated && !other.is_outdated && node.commands.size == other.node.commands.size && @@ -718,9 +732,9 @@ val markup_index = Command.Markup_Index(status, file_name) (for { chunk <- thy_load_command.chunks.get(file_name).iterator - st = state.command_state(version, thy_load_command) - res = result(st.results) - Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( + states = state.command_states(version, thy_load_command) + res = result(Command.State.merge_results(states)) + Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A]( former_range.restrict(chunk.range), info, elements, { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) } ).iterator @@ -730,9 +744,9 @@ val markup_index = Command.Markup_Index(status, "") (for { (command, command_start) <- node.command_range(former_range) - st = state.command_state(version, command) - res = result(st.results) - Text.Info(r0, a) <- st.markup(markup_index).cumulate[A]( + states = state.command_states(version, command) + res = result(Command.State.merge_results(states)) + Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A]( (former_range - command_start).restrict(command.range), info, elements, { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) diff -r cf7710540f39 -r 8201790fdeb9 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 27 10:43:43 2014 +0100 @@ -20,6 +20,9 @@ val empty: Markup_Tree = new Markup_Tree(Branches.empty) + def merge(trees: List[Markup_Tree]): Markup_Tree = + (empty /: trees)(_ ++ _) + def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree = trees match { case Nil => empty @@ -157,8 +160,12 @@ } def ++ (other: Markup_Tree): Markup_Tree = - (this /: other.branches)({ case (tree, (range, entry)) => - ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) }) + if (this eq other) this + else if (branches.isEmpty) other + else + (this /: other.branches)({ case (tree, (range, entry)) => + ((tree ++ entry.subtree) /: entry.markup)( + { case (t, elem) => t + Text.Info(range, elem) }) }) def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body = { diff -r cf7710540f39 -r 8201790fdeb9 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Pure/PIDE/protocol.scala Thu Mar 27 10:43:43 2014 +0100 @@ -117,18 +117,19 @@ var finished = 0 var warned = 0 var failed = 0 - node.commands.foreach(command => - { - val st = state.command_state(version, command) - val status = command_status(st.status) - if (status.is_running) running += 1 - else if (status.is_finished) { - if (st.results.entries.exists(p => is_warning(p._2))) warned += 1 - else finished += 1 - } - else if (status.is_failed) failed += 1 - else unprocessed += 1 - }) + for { + command <- node.commands + st <- state.command_states(version, command) + status = command_status(st.status) + } { + if (status.is_running) running += 1 + else if (status.is_finished) { + if (st.results.entries.exists(p => is_warning(p._2))) warned += 1 + else finished += 1 + } + else if (status.is_failed) failed += 1 + else unprocessed += 1 + } Node_Status(unprocessed, running, finished, warned, failed) } @@ -149,7 +150,7 @@ var commands = Map.empty[Command, Double] for { command <- node.commands.iterator - st = state.command_state(version, command) + st <- state.command_states(version, command) command_timing = (0.0 /: st.status)({ case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds diff -r cf7710540f39 -r 8201790fdeb9 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Pure/PIDE/query_operation.scala Thu Mar 27 10:43:43 2014 +0100 @@ -70,20 +70,20 @@ /* snapshot */ - val (snapshot, state, removed) = + val (snapshot, command_results, removed) = current_location match { case Some(cmd) => val snapshot = editor.node_snapshot(cmd.node_name) - val state = snapshot.state.command_state(snapshot.version, cmd) + val command_results = snapshot.state.command_results(snapshot.version, cmd) val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) - (snapshot, state, removed) + (snapshot, command_results, removed) case None => - (Document.Snapshot.init, Command.empty.init_state, true) + (Document.Snapshot.init, Command.Results.empty, true) } val results = (for { - (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries + (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries if props.contains((Markup.INSTANCE, instance)) } yield elem).toList @@ -154,7 +154,7 @@ current_update_pending = false if (current_output != new_output && !removed) { current_output = new_output - consume_output(snapshot, state.results, new_output) + consume_output(snapshot, command_results, new_output) } if (current_status != new_status) { current_status = new_status diff -r cf7710540f39 -r 8201790fdeb9 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 27 10:43:43 2014 +0100 @@ -160,8 +160,7 @@ val root = data.root for ((command, command_start) <- snapshot.node.command_range() if !stopped) { val markup = - snapshot.state.command_state(snapshot.version, command). - markup(Command.Markup_Index.markup) + snapshot.state.command_markup(snapshot.version, command, Command.Markup_Index.markup) Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start diff -r cf7710540f39 -r 8201790fdeb9 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Mar 27 10:43:43 2014 +0100 @@ -27,7 +27,8 @@ private var zoom_factor = 100 private var do_update = true private var current_snapshot = Document.Snapshot.init - private var current_state = Command.empty.init_state + private var current_command = Command.empty + private var current_results = Command.Results.empty private var current_output: List[XML.Tree] = Nil @@ -49,33 +50,34 @@ { Swing_Thread.require() - val (new_snapshot, new_state) = + val (new_snapshot, new_command, new_results) = PIDE.editor.current_node_snapshot(view) match { case Some(snapshot) => if (follow && !snapshot.is_outdated) { PIDE.editor.current_command(view, snapshot) match { case Some(cmd) => - (snapshot, snapshot.state.command_state(snapshot.version, cmd)) + (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd)) case None => - (Document.Snapshot.init, Command.empty.init_state) + (Document.Snapshot.init, Command.empty, Command.Results.empty) } } - else (current_snapshot, current_state) - case None => (current_snapshot, current_state) + else (current_snapshot, current_command, current_results) + case None => (current_snapshot, current_command, current_results) } val new_output = - if (!restriction.isDefined || restriction.get.contains(new_state.command)) { + if (!restriction.isDefined || restriction.get.contains(new_command)) { val rendering = Rendering(new_snapshot, PIDE.options.value) - rendering.output_messages(new_state) + rendering.output_messages(new_results) } else current_output if (new_output != current_output) - pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output)) + pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output)) current_snapshot = new_snapshot - current_state = new_state + current_command = new_command + current_results = new_results current_output = new_output } @@ -149,8 +151,7 @@ tooltip = "Detach window with static copy of current output" reactions += { case ButtonClicked(_) => - Info_Dockable(view, current_snapshot, - current_state.results, Pretty.separate(current_output)) + Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output)) } } diff -r cf7710540f39 -r 8201790fdeb9 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Mar 27 10:43:43 2014 +0100 @@ -592,8 +592,8 @@ message_colors.get(pri).map((_, is_separator)) } - def output_messages(st: Command.State): List[XML.Tree] = - st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList + def output_messages(results: Command.Results): List[XML.Tree] = + results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList /* text background */ diff -r cf7710540f39 -r 8201790fdeb9 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Mar 26 21:01:09 2014 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Mar 27 10:43:43 2014 +0100 @@ -26,7 +26,8 @@ /* component state -- owned by Swing thread */ private var current_snapshot = Document.State.init.snapshot() - private var current_state = Command.empty.init_state + private var current_command = Command.empty + private var current_results = Command.Results.empty private var current_id = 0L private var do_update = true private var do_auto_reply = false @@ -77,7 +78,7 @@ private def show_trace() { - val trace = Simplifier_Trace.generate_trace(current_state.results) + val trace = Simplifier_Trace.generate_trace(current_results) new Simplifier_Trace_Window(view, current_snapshot, trace) } @@ -92,7 +93,7 @@ { set_context( current_snapshot, - Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results) + Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) ) } @@ -103,23 +104,24 @@ private def handle_update(follow: Boolean) { - val (new_snapshot, new_state, new_id) = + val (new_snapshot, new_command, new_results, new_id) = PIDE.editor.current_node_snapshot(view) match { case Some(snapshot) => if (follow && !snapshot.is_outdated) { PIDE.editor.current_command(view, snapshot) match { case Some(cmd) => - (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id) + (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id) case None => - (Document.State.init.snapshot(), Command.empty.init_state, 0L) + (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L) } } - else (current_snapshot, current_state, current_id) - case None => (current_snapshot, current_state, current_id) + else (current_snapshot, current_command, current_results, current_id) + case None => (current_snapshot, current_command, current_results, current_id) } current_snapshot = new_snapshot - current_state = new_state + current_command = new_command + current_results = new_results current_id = new_id update_contents() }