more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;
--- 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 */
--- 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))
--- 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 =
{
--- 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
--- 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
--- 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
--- 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))
}
}
--- 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 */
--- 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()
}