63 |
63 |
64 /* snapshot */ |
64 /* snapshot */ |
65 |
65 |
66 val state0 = current_state.value |
66 val state0 = current_state.value |
67 |
67 |
68 val (snapshot, command_results, results, removed) = |
68 val (output, removed) = |
69 state0.location match { |
69 state0.location match { |
70 case Some(cmd) => |
70 case Some(cmd) => |
71 val snapshot = editor.node_snapshot(cmd.node_name) |
71 val snapshot = editor.node_snapshot(cmd.node_name) |
72 val command_results = snapshot.command_results(cmd) |
72 val results = snapshot.command_results(cmd) |
73 val results = |
73 val messages = |
74 List.from( |
74 List.from( |
75 for { |
75 for { |
76 case (_, elem@XML.Elem(Markup(Markup.RESULT, props@Markup.Instance(instance)), _)) |
76 case (_, msg@XML.Elem(Markup(Markup.RESULT, props@Markup.Instance(instance)), _)) |
77 <- command_results.iterator |
77 <- results.iterator |
78 if instance == state0.instance |
78 if instance == state0.instance |
79 } yield elem) |
79 } yield msg) |
80 val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd) |
80 val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd) |
81 (snapshot, command_results, results, removed) |
81 (Editor.Output(snapshot, results, messages), removed) |
82 case None => |
82 case None => (Editor.Output.init, true) |
83 (Document.Snapshot.init, Command.Results.empty, Nil, true) |
|
84 } |
83 } |
85 |
84 |
86 |
85 |
87 |
86 |
88 /* resolve sendback: static command id */ |
87 /* resolve sendback: static command id */ |
112 |
111 |
113 /* output */ |
112 /* output */ |
114 |
113 |
115 val new_output = |
114 val new_output = |
116 for { |
115 for { |
117 case XML.Elem(_, List(XML.Elem(markup, body))) <- results |
116 case XML.Elem(_, List(XML.Elem(markup, body))) <- output.messages |
118 if Markup.messages.contains(markup.name) |
117 if Markup.messages.contains(markup.name) |
119 body1 = resolve_sendback(body) |
118 body1 = resolve_sendback(body) |
120 } yield Protocol.make_message(body1, markup.name, props = markup.properties) |
119 } yield Protocol.make_message(body1, markup.name, props = markup.properties) |
121 |
120 |
122 |
121 |
123 /* status */ |
122 /* status */ |
124 |
123 |
125 def get_status(name: String, status: Query_Operation.Status): Option[Query_Operation.Status] = |
124 def get_status(name: String, status: Query_Operation.Status): Option[Query_Operation.Status] = |
126 results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
125 output.messages.collectFirst( |
|
126 { case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) |
127 |
127 |
128 val new_status = |
128 val new_status = |
129 if (removed) Query_Operation.Status.finished |
129 if (removed) Query_Operation.Status.finished |
130 else |
130 else |
131 get_status(Markup.FINISHED, Query_Operation.Status.finished) orElse |
131 get_status(Markup.FINISHED, Query_Operation.Status.finished) orElse |
134 |
134 |
135 |
135 |
136 /* state update */ |
136 /* state update */ |
137 |
137 |
138 if (new_status == Query_Operation.Status.running) |
138 if (new_status == Query_Operation.Status.running) |
139 results.collectFirst( |
139 output.messages.collectFirst( |
140 { |
140 { |
141 case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) |
141 case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) |
142 if elem.name == Markup.RUNNING => id |
142 if elem.name == Markup.RUNNING => id |
143 }).foreach(id => current_state.change(_.copy(exec_id = id))) |
143 }).foreach(id => current_state.change(_.copy(exec_id = id))) |
144 |
144 |
145 if (state0.output != new_output || state0.status != new_status) { |
145 if (state0.output != new_output || state0.status != new_status) { |
146 if (snapshot.is_outdated) { |
146 if (output.snapshot.is_outdated) { |
147 current_state.change(_.copy(update_pending = true)) |
147 current_state.change(_.copy(update_pending = true)) |
148 } |
148 } |
149 else { |
149 else { |
150 current_state.change(_.copy(update_pending = false)) |
150 current_state.change(_.copy(update_pending = false)) |
151 if (state0.output != new_output && !removed) { |
151 if (state0.output != new_output && !removed) { |
152 current_state.change(_.copy(output = new_output)) |
152 current_state.change(_.copy(output = new_output)) |
153 consume_output( |
153 consume_output(output.copy(messages = new_output)) |
154 Editor.Output(snapshot = snapshot, results = command_results, messages = new_output)) |
|
155 } |
154 } |
156 if (state0.status != new_status) { |
155 if (state0.status != new_status) { |
157 current_state.change(_.copy(status = new_status)) |
156 current_state.change(_.copy(status = new_status)) |
158 consume_status(new_status) |
157 consume_status(new_status) |
159 if (new_status == Query_Operation.Status.finished) |
158 if (new_status == Query_Operation.Status.finished) |