| changeset 61721 | e37046b121a2 |
| parent 61720 | a31730632e13 |
| child 61726 | 04f8564d6983 |
| 61720:a31730632e13 | 61721:e37046b121a2 |
|---|---|
55 } |
55 } |
56 |
56 |
57 |
57 |
58 /* update */ |
58 /* update */ |
59 |
59 |
60 private var do_update = true |
60 private var do_update = false |
61 |
61 |
62 private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() } |
62 private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() } |
63 |
63 |
64 def update() |
64 def update() |
65 { |
65 { |