equal
deleted
inserted
replaced
134 |
134 |
135 if (theories_result.ok) session_result |
135 if (theories_result.ok) session_result |
136 else { |
136 else { |
137 for { |
137 for { |
138 (name, status) <- theories_result.nodes if !status.ok |
138 (name, status) <- theories_result.nodes if !status.ok |
139 (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree) |
139 (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree) |
140 } progress.echo_error_message(XML.content(Pretty.formatted(List(tree)))) |
140 } progress.echo_error_message(XML.content(Pretty.formatted(List(tree)))) |
141 |
141 |
142 session_result.copy(rc = session_result.rc max 1) |
142 session_result.copy(rc = session_result.rc max 1) |
143 } |
143 } |
144 } |
144 } |