# HG changeset patch # User wenzelm # Date 1527684364 -7200 # Node ID 7eaaa8f48331a52fd6ccf3eb72ecea3196039e27 # Parent d7920eb7de54d490ca3bd7ad4a811af3a827dace clarified outermost progress.interrupt_handler; diff -r d7920eb7de54 -r 7eaaa8f48331 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Wed May 30 14:34:43 2018 +0200 +++ b/src/Pure/ML/ml_console.scala Wed May 30 14:46:04 2018 +0200 @@ -54,8 +54,10 @@ if (!no_build && !raw_ml_system) { val progress = new Console_Progress() val rc = - Build.build_logic(options, logic, build_heap = true, progress = progress, - dirs = dirs, system_mode = system_mode) + progress.interrupt_handler { + Build.build_logic(options, logic, build_heap = true, progress = progress, + dirs = dirs, system_mode = system_mode) + } if (rc != 0) sys.exit(rc) } diff -r d7920eb7de54 -r 7eaaa8f48331 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Wed May 30 14:34:43 2018 +0200 +++ b/src/Pure/Thy/export.scala Wed May 30 14:46:04 2018 +0200 @@ -288,8 +288,10 @@ if (!no_build) { val rc = - Build.build_logic(options, session_name, progress = progress, - dirs = dirs, system_mode = system_mode) + progress.interrupt_handler { + Build.build_logic(options, session_name, progress = progress, + dirs = dirs, system_mode = system_mode) + } if (rc != 0) sys.exit(rc) } diff -r d7920eb7de54 -r 7eaaa8f48331 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed May 30 14:34:43 2018 +0200 +++ b/src/Pure/Tools/build.scala Wed May 30 14:46:04 2018 +0200 @@ -836,10 +836,8 @@ system_mode = system_mode, sessions = List(logic)).ok) 0 else { progress.echo("Build started for Isabelle/" + logic + " ...") - progress.interrupt_handler { - Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs, - system_mode = system_mode, sessions = List(logic)).rc - } + Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs, + system_mode = system_mode, sessions = List(logic)).rc } } } diff -r d7920eb7de54 -r 7eaaa8f48331 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Wed May 30 14:34:43 2018 +0200 +++ b/src/Pure/Tools/dump.scala Wed May 30 14:46:04 2018 +0200 @@ -172,21 +172,23 @@ val progress = new Console_Progress(verbose = verbose) val result = - dump(options, logic, - aspects = aspects, - progress = progress, - dirs = dirs, - select_dirs = select_dirs, - output_dir = output_dir, - verbose = verbose, - 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, + verbose = verbose, + 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.echo(result.timing.message_resources)