equal
deleted
inserted
replaced
30 |
30 |
31 object Ignore_Progress extends Progress |
31 object Ignore_Progress extends Progress |
32 |
32 |
33 class Console_Progress(verbose: Boolean) extends Progress |
33 class Console_Progress(verbose: Boolean) extends Progress |
34 { |
34 { |
35 override def echo(msg: String) { System.out.println(msg) } |
35 override def echo(msg: String) { Console.println(msg) } |
36 override def theory(session: String, theory: String): Unit = |
36 override def theory(session: String, theory: String): Unit = |
37 if (verbose) echo(session + ": theory " + theory) |
37 if (verbose) echo(session + ": theory " + theory) |
38 |
38 |
39 @volatile private var is_stopped = false |
39 @volatile private var is_stopped = false |
40 def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e } |
40 def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e } |