equal
deleted
inserted
replaced
25 def state = _state |
25 def state = _state |
26 |
26 |
27 override def act() { |
27 override def act() { |
28 loop { |
28 loop { |
29 react { |
29 react { |
30 case message: XML.Tree => _state += message |
30 case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message) |
|
31 case bad => System.err.println("prover: ignoring bad message " + bad) |
31 } |
32 } |
32 } |
33 } |
33 } |
34 } |
34 } |
35 } |
35 |
36 |
50 } |
51 } |
51 |
52 |
52 |
53 |
53 class Command( |
54 class Command( |
54 val tokens: List[Token], |
55 val tokens: List[Token], |
55 val starts: Map[Token, Int], |
56 val starts: Map[Token, Int]) extends Accumulator |
56 change_receiver: Actor) extends Accumulator |
|
57 { |
57 { |
58 require(!tokens.isEmpty) |
58 require(!tokens.isEmpty) |
59 |
59 |
60 val id = Isabelle.system.id() |
60 val id = Isabelle.system.id() |
61 override def hashCode = id.hashCode |
61 override def hashCode = id.hashCode |
62 |
|
63 def changed() = change_receiver ! this |
|
64 |
62 |
65 |
63 |
66 /* content */ |
64 /* content */ |
67 |
65 |
68 override def toString = name |
66 override def toString = name |