diff -r 87ebf5a50283 -r 42267c650205 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Apr 01 17:06:10 2022 +0200 +++ b/src/Pure/Tools/dump.scala Fri Apr 01 23:19:12 2022 +0200 @@ -298,37 +298,37 @@ 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 - val name = snapshot.node_name - if (status.ok) { - try { - if (context.process_theory(name.theory)) { - process_theory(Args(session, 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)) :: _) + Consumer_Thread.fork(name = "dump")(consume = + { (args: (Document.Snapshot, Document_Status.Node_Status)) => + val (snapshot, status) = args + val name = snapshot.node_name + if (status.ok) { + try { + if (context.process_theory(name.theory)) { + process_theory(Args(session, snapshot, status)) } } - else { - val msgs = - for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem)) - yield { - "Error" + Position.here(pos) + ":\n" + - XML.content(Pretty.formatted(List(elem))) - } - progress.echo("FAILED to process theory " + name) - msgs.foreach(progress.echo_error_message) - consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) + 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)) :: _) } - true - }) + } + else { + val msgs = + for ((elem, pos) <- snapshot.messages if Protocol.is_error(elem)) + yield { + "Error" + Position.here(pos) + ":\n" + + XML.content(Pretty.formatted(List(elem))) + } + progress.echo("FAILED to process theory " + name) + msgs.foreach(progress.echo_error_message) + consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) + } + true + }) def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = consumer.send((snapshot, status)) @@ -393,13 +393,13 @@ context.build_logic(logic) for (session <- context.sessions(logic = logic, log = log)) { - session.process((args: Args) => { - progress.echo("Processing theory " + args.print_node + " ...") - val aspect_args = - Aspect_Args(session.options, context.deps, progress, output_dir, - args.snapshot, args.status) - aspects.foreach(_.operation(aspect_args)) - }) + session.process({ (args: Args) => + progress.echo("Processing theory " + args.print_node + " ...") + val aspect_args = + Aspect_Args(session.options, context.deps, progress, output_dir, + args.snapshot, args.status) + aspects.foreach(_.operation(aspect_args)) + }) } context.check_errors @@ -410,22 +410,22 @@ val isabelle_tool = Isabelle_Tool("dump", "dump cumulative PIDE session database", Scala_Project.here, - args => { - var aspects: List[Aspect] = known_aspects - var base_sessions: List[String] = Nil - var select_dirs: List[Path] = Nil - var output_dir = default_output_dir - var requirements = false - var exclude_session_groups: List[String] = Nil - var all_sessions = false - var logic = default_logic - var dirs: List[Path] = Nil - var session_groups: List[String] = Nil - var options = Options.init() - var verbose = false - var exclude_sessions: List[String] = Nil + { args => + var aspects: List[Aspect] = known_aspects + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var output_dir = default_output_dir + var requirements = false + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var logic = default_logic + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var options = Options.init() + var verbose = false + var exclude_sessions: List[String] = Nil - val getopts = Getopts(""" + val getopts = Getopts(""" Usage: isabelle dump [OPTIONS] [SESSIONS ...] Options are: @@ -446,49 +446,49 @@ Dump cumulative PIDE session database, with the following aspects: """ + Library.indent_lines(4, show_aspects) + "\n", - "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)), - "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), - "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), - "O:" -> (arg => output_dir = Path.explode(arg)), - "R" -> (_ => requirements = true), - "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), - "a" -> (_ => all_sessions = true), - "b:" -> (arg => logic = arg), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "g:" -> (arg => session_groups = session_groups ::: List(arg)), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose = true), - "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)), + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "O:" -> (arg => output_dir = Path.explode(arg)), + "R" -> (_ => requirements = true), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "b:" -> (arg => logic = arg), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) - val sessions = getopts(args) + val sessions = getopts(args) - val progress = new Console_Progress(verbose = verbose) + val progress = new Console_Progress(verbose = verbose) - val start_date = Date.now() + val start_date = Date.now() - progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date)) + progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date)) - 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)) - } + 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)) + } - val end_date = Date.now() - val timing = end_date.time - start_date.time + val end_date = Date.now() + val timing = end_date.time - start_date.time - progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date)) - progress.echo(timing.message_hms + " elapsed time") - }) + progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date)) + progress.echo(timing.message_hms + " elapsed time") + }) }