# HG changeset patch # User wenzelm # Date 1546091931 -3600 # Node ID e3a9680d9ed8062746b1c35a46e5d56d2248b442 # Parent 913970ae232464fe1d6cd1d05afca1011f0d218d clarified errors, according to Isabelle/MMT; tuned signature; diff -r 913970ae2324 -r e3a9680d9ed8 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sat Dec 29 13:49:09 2018 +0100 +++ b/src/Pure/Tools/dump.scala Sat Dec 29 14:58:51 2018 +0100 @@ -76,13 +76,13 @@ /* session */ def session(dump_options: Options, logic: String, - consume: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit, + process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit, progress: Progress = No_Progress, log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, system_mode: Boolean = false, - selection: Sessions.Selection = Sessions.Selection.empty): Boolean = + selection: Sessions.Selection = Sessions.Selection.empty) { /* dependencies */ @@ -91,25 +91,48 @@ selection_deps(dump_options, selection, progress = progress, uniform_session = true, loading_sessions = true) + val use_theories = + for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) } + yield name.theory - /* dump aspects asynchronously */ + + /* asynchronous consumer */ object Consumer { - private val consumer_ok = Synchronized(true) + sealed case class Bad_Theory( + name: Document.Node.Name, + status: Document_Status.Node_Status, + errors: List[String]) + + private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory]) private val consumer = Consumer_Thread.fork(name = "dump")( consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => { val (snapshot, status) = args - if (status.ok) consume(deps, snapshot, status) + val name = snapshot.node_name + if (status.ok) { + try { process_theory(deps, snapshot, status) } + catch { + case exn: Throwable if !Exn.is_interrupt(exn) => + val msg = Exn.message(exn) + progress.echo("FAILED to process theory " + name) + progress.echo_error_message(msg) + consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _) + } + } else { - consumer_ok.change(_ => false) - for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) { - val msg = XML.content(Pretty.formatted(List(tree))) - progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg) - } + val msgs = + for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) + yield { + "Error" + Position.here(pos) + ":\n" + + XML.content(Pretty.formatted(List(tree))) + } + progress.echo("FAILED to process theory " + name) + msgs.foreach(progress.echo_error_message) + consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) } true }) @@ -117,10 +140,10 @@ def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = consumer.send((snapshot, status)) - def shutdown(): Boolean = + def shutdown(): List[Bad_Theory] = { consumer.shutdown() - consumer_ok.value + consumer_bad_theories.value.reverse } } @@ -132,23 +155,28 @@ session_dirs = dirs ::: select_dirs, include_sessions = deps.sessions_structure.imports_topological_order) - val use_theories = - for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) } - yield name.theory - - val use_theories_result = - session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _)) - - session.stop() + try { + val use_theories_result = + session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _)) - val consumer_ok = Consumer.shutdown() + val bad_theories = Consumer.shutdown() + val bad_msgs = + bad_theories.map(bad => + Output.clean_yxml( + "FAILED theory " + bad.name + + (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") + + (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", "")))) - use_theories_result.nodes_pending match { - case Nil => - case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString))) + val pending_msgs = + use_theories_result.nodes_pending match { + case Nil => Nil + case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString))) + } + + val errors = bad_msgs ::: pending_msgs + if (errors.nonEmpty) error(errors.mkString("\n\n")) } - - use_theories_result.ok && consumer_ok + finally { session.stop() } } @@ -173,14 +201,14 @@ select_dirs: List[Path] = Nil, output_dir: Path = default_output_dir, system_mode: Boolean = false, - selection: Sessions.Selection = Sessions.Selection.empty): Boolean = + selection: Sessions.Selection = Sessions.Selection.empty) { if (Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED") val dump_options = make_options(options, aspects) - def consume( + def process_theory( deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) @@ -189,7 +217,7 @@ aspects.foreach(_.operation(aspect_args)) } - session(dump_options, logic, consume _, + session(dump_options, logic, process_theory _, progress = progress, log = log, dirs = dirs, select_dirs = select_dirs, selection = selection) } @@ -255,24 +283,21 @@ val progress = new Console_Progress(verbose = verbose) - val ok = - progress.interrupt_handler { - dump(options, logic, - aspects = aspects, - progress = progress, - dirs = dirs, - select_dirs = select_dirs, - output_dir = output_dir, - selection = Sessions.Selection( - requirements = requirements, - all_sessions = all_sessions, - base_sessions = base_sessions, - exclude_session_groups = exclude_session_groups, - exclude_sessions = exclude_sessions, - session_groups = session_groups, - sessions = sessions)) - } - - if (!ok) sys.exit(2) + progress.interrupt_handler { + dump(options, logic, + aspects = aspects, + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + output_dir = output_dir, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions)) + } }) }