equal
deleted
inserted
replaced
17 import scala.annotation.tailrec |
17 import scala.annotation.tailrec |
18 |
18 |
19 |
19 |
20 object Build |
20 object Build |
21 { |
21 { |
22 /** progress context **/ |
|
23 |
|
24 class Progress |
|
25 { |
|
26 def echo(msg: String) {} |
|
27 def theory(session: String, theory: String) {} |
|
28 def stopped: Boolean = false |
|
29 override def toString: String = if (stopped) "Progress(stopped)" else "Progress" |
|
30 } |
|
31 |
|
32 object Ignore_Progress extends Progress |
|
33 |
|
34 class Console_Progress(verbose: Boolean = false) extends Progress |
|
35 { |
|
36 override def echo(msg: String) { Console.println(msg) } |
|
37 override def theory(session: String, theory: String): Unit = |
|
38 if (verbose) echo(session + ": theory " + theory) |
|
39 |
|
40 @volatile private var is_stopped = false |
|
41 def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e } |
|
42 override def stopped: Boolean = |
|
43 { |
|
44 if (Thread.interrupted) is_stopped = true |
|
45 is_stopped |
|
46 } |
|
47 } |
|
48 |
|
49 |
|
50 |
|
51 /** session information **/ |
22 /** session information **/ |
52 |
23 |
53 // external version |
24 // external version |
54 abstract class Entry |
25 abstract class Entry |
55 sealed case class Chapter(name: String) extends Entry |
26 sealed case class Chapter(name: String) extends Entry |