changeset 67880 | e59220a075de |
parent 65827 | 3bba3856b56c |
child 73340 | 0ffcad1f6130 |
--- a/src/Pure/Tools/check_keywords.scala Fri Mar 16 16:28:03 2018 +0100 +++ b/src/Pure/Tools/check_keywords.scala Fri Mar 16 16:38:46 2018 +0100 @@ -41,7 +41,7 @@ val bad = Par_List.map((arg: (String, Token.Pos)) => { - if (progress.stopped) throw Exn.Interrupt() + progress.expose_interrupt() conflicts(keywords, check, arg._1, arg._2) }, parallel_args).flatten