more reactive interrupts;
authorwenzelm
Wed Apr 01 17:20:52 2015 +0200 (2015-04-01)
changeset 5989389f3bd11fa8b
parent 59892 2a616319c171
child 59894 ca16b657901f
more reactive interrupts;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 16:24:38 2015 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 17:20:52 2015 +0200
     1.3 @@ -508,13 +508,14 @@
     1.4                progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
     1.5  
     1.6              if (check_keywords.nonEmpty) {
     1.7 -              for {
     1.8 -                path <- theory_files
     1.9 -                (tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path)
    1.10 -              } {
    1.11 -                progress.echo(Output.warning_text(
    1.12 -                  "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
    1.13 -                    Position.here(pos)))
    1.14 +              for (path <- theory_files) {
    1.15 +                if (progress.stopped) throw Exn.Interrupt()
    1.16 +                for ((tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path))
    1.17 +                {
    1.18 +                  progress.echo(Output.warning_text(
    1.19 +                    "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
    1.20 +                      Position.here(pos)))
    1.21 +                }
    1.22                }
    1.23              }
    1.24