# HG changeset patch
# User wenzelm
# Date 1521214726 -3600
# Node ID e59220a075dec219a2947889b609a03a37fc19fa
# Parent  e4903b803b8b4cd1e170e67770216ae9bbda9d0f
tuned signature;

diff -r e4903b803b8b -r e59220a075de src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Fri Mar 16 16:28:03 2018 +0100
+++ b/src/Pure/System/progress.scala	Fri Mar 16 16:38:46 2018 +0100
@@ -23,6 +23,7 @@
     Timing.timeit(message, enabled, echo(_))(e)
 
   def stopped: Boolean = false
+  def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
   def bash(script: String,
diff -r e4903b803b8b -r e59220a075de src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Mar 16 16:28:03 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Mar 16 16:38:46 2018 +0100
@@ -227,7 +227,7 @@
     val session_bases =
       (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
         case (session_bases, session_name) =>
-          if (progress.stopped) throw Exn.Interrupt()
+          progress.expose_interrupt()
 
           val info = sessions_structure(session_name)
           try {
diff -r e4903b803b8b -r e59220a075de src/Pure/Tools/check_keywords.scala
--- 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