# 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)