68 Swing_Thread.require() |
68 Swing_Thread.require() |
69 |
69 |
70 |
70 |
71 /* snapshot */ |
71 /* snapshot */ |
72 |
72 |
73 val (snapshot, state, removed) = |
73 val (snapshot, command_results, removed) = |
74 current_location match { |
74 current_location match { |
75 case Some(cmd) => |
75 case Some(cmd) => |
76 val snapshot = editor.node_snapshot(cmd.node_name) |
76 val snapshot = editor.node_snapshot(cmd.node_name) |
77 val state = snapshot.state.command_state(snapshot.version, cmd) |
77 val command_results = snapshot.state.command_results(snapshot.version, cmd) |
78 val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) |
78 val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) |
79 (snapshot, state, removed) |
79 (snapshot, command_results, removed) |
80 case None => |
80 case None => |
81 (Document.Snapshot.init, Command.empty.init_state, true) |
81 (Document.Snapshot.init, Command.Results.empty, true) |
82 } |
82 } |
83 |
83 |
84 val results = |
84 val results = |
85 (for { |
85 (for { |
86 (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries |
86 (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.entries |
87 if props.contains((Markup.INSTANCE, instance)) |
87 if props.contains((Markup.INSTANCE, instance)) |
88 } yield elem).toList |
88 } yield elem).toList |
89 |
89 |
90 |
90 |
91 /* resolve sendback: static command id */ |
91 /* resolve sendback: static command id */ |
152 current_update_pending = true |
152 current_update_pending = true |
153 else { |
153 else { |
154 current_update_pending = false |
154 current_update_pending = false |
155 if (current_output != new_output && !removed) { |
155 if (current_output != new_output && !removed) { |
156 current_output = new_output |
156 current_output = new_output |
157 consume_output(snapshot, state.results, new_output) |
157 consume_output(snapshot, command_results, new_output) |
158 } |
158 } |
159 if (current_status != new_status) { |
159 if (current_status != new_status) { |
160 current_status = new_status |
160 current_status = new_status |
161 consume_status(new_status) |
161 consume_status(new_status) |
162 if (new_status == Query_Operation.Status.FINISHED) |
162 if (new_status == Query_Operation.Status.FINISHED) |