equal
deleted
inserted
replaced
93 } |
93 } |
94 |
94 |
95 |
95 |
96 /* painting */ |
96 /* painting */ |
97 |
97 |
98 val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all()) |
98 val repaint_delay = Delay(100){ repaint_all() } |
99 |
99 |
100 val change_receiver = actor { |
100 val change_receiver = actor { |
101 loop { |
101 loop { |
102 react { |
102 react { |
103 case _ => { // FIXME potentially blocking within loop/react!?!?!?! |
103 case _ => { // FIXME potentially blocking within loop/react!?!?!?! |
104 Swing_Thread.now { |
104 Swing_Thread.now { |
105 repaint_delay.delay_or_ignore() |
105 repaint_delay.prod() |
106 phase_overview.repaint_delay.delay_or_ignore() |
106 phase_overview.repaint_delay.prod() |
107 } |
107 } |
108 } |
108 } |
109 } |
109 } |
110 } |
110 } |
111 } |
111 } |