src/Pure/System/progress.scala

--- a/src/Pure/System/progress.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/System/progress.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -36,8 +36,15 @@
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)
 
-  def stopped: Boolean = false
-  def interrupt_handler[A](e: => A): A = e
+  @volatile protected var is_stopped = false
+  def stop { is_stopped = true }
+  def stopped: Boolean =
+  {
+    if (Thread.interrupted) is_stopped = true
+    is_stopped
+  }
+
+  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
   def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
@@ -55,8 +62,6 @@
   }
 }
 
-object No_Progress extends Progress
-
 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 {
   override def echo(msg: String): Unit =
@@ -64,15 +69,6 @@
 
   override def theory(theory: Progress.Theory): Unit =
     if (verbose) echo(theory.message)
-
-  @volatile private var is_stopped = false
-  override def interrupt_handler[A](e: => A): A =
-    POSIX_Interrupt.handler { is_stopped = true } { e }
-  override def stopped: Boolean =
-  {
-    if (Thread.interrupted) is_stopped = true
-    is_stopped
-  }
 }
 
 class File_Progress(path: Path, verbose: Boolean = false) extends Progress