# HG changeset patch
# User wenzelm
# Date 1427901652 -7200
# Node ID 89f3bd11fa8b126a782d19804105ce3ce192e503
# Parent  2a616319c17161aa1adb4c36ae119bb90d0264ae
more reactive interrupts;

diff -r 2a616319c171 -r 89f3bd11fa8b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 16:24:38 2015 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 17:20:52 2015 +0200
@@ -508,13 +508,14 @@
               progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
 
             if (check_keywords.nonEmpty) {
-              for {
-                path <- theory_files
-                (tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path)
-              } {
-                progress.echo(Output.warning_text(
-                  "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
-                    Position.here(pos)))
+              for (path <- theory_files) {
+                if (progress.stopped) throw Exn.Interrupt()
+                for ((tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path))
+                {
+                  progress.echo(Output.warning_text(
+                    "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
+                      Position.here(pos)))
+                }
               }
             }