equal
deleted
inserted
replaced
114 if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories)) |
114 if (bad_theories.nonEmpty) error("Unknown theories " + commas_quote(bad_theories)) |
115 |
115 |
116 val print_theories = |
116 val print_theories = |
117 if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
117 if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) |
118 for (thy <- print_theories) { |
118 for (thy <- print_theories) { |
119 val thy_heading = "Theory " + quote(thy) + ":" |
119 val thy_heading = "\nTheory " + quote(thy) + ":" |
120 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |
120 read_theory(db_context, resources, session_name, thy, unicode_symbols = unicode_symbols) |
121 match { |
121 match { |
122 case None => progress.echo(thy_heading + " MISSING") |
122 case None => progress.echo(thy_heading + " MISSING") |
123 case Some(command) => |
123 case Some(command) => |
124 val snapshot = Document.State.init.command_snippet(command) |
124 val snapshot = Document.State.init.command_snippet(command) |
135 } |
135 } |
136 } |
136 } |
137 |
137 |
138 if (errors.nonEmpty) { |
138 if (errors.nonEmpty) { |
139 val msg = Symbol.output(unicode_symbols, cat_lines(errors)) |
139 val msg = Symbol.output(unicode_symbols, cat_lines(errors)) |
140 progress.echo("\nErrors:\n" + Output.error_message_text(msg)) |
140 progress.echo("\nBuild errors:\n" + Output.error_message_text(msg)) |
141 } |
141 } |
142 if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc)) |
142 if (rc != 0) progress.echo("\n" + Process_Result.print_return_code(rc)) |
143 } |
143 } |
144 }) |
144 }) |
145 } |
145 } |