--- 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