| 61276 |      1 | /*  Title:      Pure/System/progress.scala
 | 
|  |      2 |     Author:     Makarius
 | 
|  |      3 | 
 | 
|  |      4 | Progress context for system processes.
 | 
|  |      5 | */
 | 
|  |      6 | 
 | 
|  |      7 | package isabelle
 | 
|  |      8 | 
 | 
|  |      9 | 
 | 
|  |     10 | class Progress
 | 
|  |     11 | {
 | 
|  |     12 |   def echo(msg: String) {}
 | 
|  |     13 |   def theory(session: String, theory: String) {}
 | 
|  |     14 |   def stopped: Boolean = false
 | 
|  |     15 |   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 | 
|  |     16 | }
 | 
|  |     17 | 
 | 
|  |     18 | object Ignore_Progress extends Progress
 | 
|  |     19 | 
 | 
|  |     20 | class Console_Progress(verbose: Boolean = false) extends Progress
 | 
|  |     21 | {
 | 
|  |     22 |   override def echo(msg: String) { Console.println(msg) }
 | 
|  |     23 |   override def theory(session: String, theory: String): Unit =
 | 
|  |     24 |     if (verbose) echo(session + ": theory " + theory)
 | 
|  |     25 | 
 | 
|  |     26 |   @volatile private var is_stopped = false
 | 
|  |     27 |   def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
 | 
|  |     28 |   override def stopped: Boolean =
 | 
|  |     29 |   {
 | 
|  |     30 |     if (Thread.interrupted) is_stopped = true
 | 
|  |     31 |     is_stopped
 | 
|  |     32 |   }
 | 
|  |     33 | }
 |